Mercurial > hg > Papers > 2021 > soto-thesis
changeset 14:a63df15c9afc default tip
DONE
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 15 Feb 2021 23:36:39 +0900 |
| parents | 4361e7b7d3db |
| children | |
| files | paper/final_thesis.pdf paper/soto.bib paper/tex/agda.tex paper/tex/cbc_agda.tex paper/tex/rbt_imple.tex paper/tex/rbt_verif.tex paper/tex/thanks.tex slide/slide.html slide/slide.pdf |
| diffstat | 9 files changed, 149 insertions(+), 1036 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/soto.bib Mon Feb 15 21:42:10 2021 +0900 +++ b/paper/soto.bib Mon Feb 15 23:36:39 2021 +0900 @@ -64,7 +64,23 @@ school = "琉球大学 大学院理工学研究科 情報工学専攻", year = "2016" } - + +@inproceedings{mitsuki-prosym, + author = "宮城光希 and 河野真治", + title = "Code Gear と Data Gear を持つ Gears OS の設計", + booktitle = "第59回プログラミング・シンポジウム予稿集", + year = "2018", + volume = "2018", + pages = "197--206", + month = "jan" +} + +@misc{cbc-llvm, + title = {cbc-llvm - 並列信頼研 mercurial repository}, + howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_llvm/}}, + note = {Accessed: 2020/2/9(Sun)} +} + @misc{rbtree, title={データ構造と基本アルゴリズム}, author={渡邉},
--- a/paper/tex/agda.tex Mon Feb 15 21:42:10 2021 +0900 +++ b/paper/tex/agda.tex Mon Feb 15 23:36:39 2021 +0900 @@ -40,16 +40,16 @@ y が 0 になった際に計算が終了となっている。 指折りでの足し算を実装していると捉えても良い。 -\subsection{三項演算子の実装} +\subsection{二項演算子の実装} \_ (アンダースコア) を用いることで入力を受け取る事ができる。 -これを用いることで、三項演算子を実装することができる。 -以下に、三項演算子を使用した \coderef{plus} と同義の関数の例を +これを用いることで、二項演算子を実装することができる。 +以下に、二項演算子を使用した \coderef{plus} と同義の関数の例を 以下 \coderef{plus2} 挙げる。 -\lstinputlisting[label=plus2, caption=三項演算子を用いたplusの実装, firstline=5] {src/agda/plus2.agda} +\lstinputlisting[label=plus2, caption=二項演算子を用いたplusの実装, firstline=5] {src/agda/plus2.agda} 利点としては、直感的な記号論理の記述ができる。 -以下、記号論理は基本的に三項演算子を使用して記述する。 +以下、記号論理は基本的に二項演算子を使用して記述する。 \begin{comment} \subsection{Agdaにおけるラムダ計算} @@ -78,17 +78,14 @@ \subsection{Record 型の実装} Record 型とはオブジェクトあるいは構造体ののようなものである。 -\coderef{And}は AND の関数となる。p1で前方部分が取得でき、p2で後方部分が取得できる。 - -\lstinputlisting[label=And の定義, caption=And] {src/agda/And.agda} +\coderef{Andの定義}は AND の関数となる。p1で前方部分が取得でき、p2で後方部分が取得できる。 -また、Agda の関数定義では\_(アンダースコア)で囲むことで三項演算子を定義することができる。 +\lstinputlisting[label=Andの定義, caption=Andの記述] {src/agda/And.agda} -これを使用して三段論法を定義することができる。 定義は「AならばB」かつ「BならばC」なら「AならばC」となる。 \coderef{syllogism}を以下に示す。 -\lstinputlisting[label=syllogism の実装, caption=syllogism] {src/agda/syllogism.agda} +\lstinputlisting[label=syllogism, caption=syllogism の記述] {src/agda/syllogism.agda} コードの解説をすると、引数として x と a が関数に与えられている。 引数 x の中身は ((A $ \rightarrow $ B) ∧ (B $ \rightarrow $ C)) 、引数 a の中身 @@ -97,7 +94,7 @@ よって A を与えて C を取得することができたため、三段論法を定義できた。 \section{本論で使用する Agda の記法} -本論では、ソースコードを出しながら実施内容について述べるが、 +本論では、ソースコードを出し、それの実施内容について述べるが、 特殊な記法を用いている場合があるので、前もって解説をする。 \subsection{Agdaの省略記法} @@ -106,6 +103,8 @@ これを防ぐために、withを使用し、必要な変数のみ取り出してパターンマッチを行う。 例を \coderef{abridgement} に示す。 +\newpage + \lstinputlisting[label=abridgement, caption=入力を省略する Agda コードの例, firstline=5] {src/agda/abridgement.agda} patternmatch-default は入力されている record をそのまま展開することで、
--- a/paper/tex/cbc_agda.tex Mon Feb 15 21:42:10 2021 +0900 +++ b/paper/tex/cbc_agda.tex Mon Feb 15 23:36:39 2021 +0900 @@ -1,10 +1,6 @@ \chapter{Continuation based C と Agda} -\section{検証手法} -本章では検証する際の手法を説明する。 -CodeGear の引数となる DataGear が事前条件となり、 -それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。 -その後、さらに事後条件となる DetaGear も Meta Gears にて検証する。 -これらを用いて Hoare Logic によりプログラムの検証を行いたい。 +\section{記述手法} +本章では CbC に対応した Agda を記述する際の手法を説明する。 \subsection{GearsAgda 形式で書く agda} Agdaでは関数の再帰呼び出しが可能であるが、CbCでは値が 帰って来ない。そのためAgda @@ -21,7 +17,7 @@ Env と next と exit を受け取っている。 next と next は Env → t となっているが、 -これは env を受け取って不定の型 (t) を返すという意味である。 +これは Env を受け取って不定の型 (t) を返すという意味である。 これで 次の関数遷移先を取れるようにしている。 @@ -33,8 +29,8 @@ CbCでは再起処理を実装することはできないが、自己呼び出しを行うことはできるので、 それに合ったようにAgdaでも実装を行なう。 -17行目が実際に値を入れる部分になっています。 -Exitが実行の終了になるようにしています。 +17行目が実際に値を入れる部分で、 +Exitが実行の終了になるようにしている。 前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。 これがAgdaで表現された CodeGear となり、本論では Gears Agda と呼ぶ
--- a/paper/tex/rbt_imple.tex Mon Feb 15 21:42:10 2021 +0900 +++ b/paper/tex/rbt_imple.tex Mon Feb 15 23:36:39 2021 +0900 @@ -1,6 +1,6 @@ \chapter{Red Black Tree の実装} -Left Learning Red Blacl Tree の実装において、 +Left Learning Red Black Tree の実装において、 通常の言語であれば再起処理を用いて実装を行える部分を 継続にて実行可能なように変更する必要がある。 本節では、この課題に対して Gears Agda での @@ -12,14 +12,13 @@ \begin{figure}[H] \begin{center} - \includegraphics[height=7.5cm]{pic/imple/実装.pdf} + \includegraphics[height=7.5cm]{pic/imple.pdf} \end{center} \caption{再起処理を回避する手順} \label{rbt_imple} \end{figure} -41の値を Left Leaning Red Black Tree に insert もしくは delete する際の手順を説 -明する。 +41の値を Left Leaning Red Black Tree に insert もしくは delete する際の手順を説明する。 まず Root node である 59 と比較した際に、41はそれより小さい。 この際、left node に遷移するが、CbC では再起処理が行えないため、listに保持していく。 順々に辿っていき、対象の場所に到達すると insert / delete を行う。 @@ -34,13 +33,14 @@ 箇条書きにてそれぞれについて解説を行う。 -\begin{description} -\item[col] 色のことで、red と black の data 型で記述し、パターンマッチを行えるようにした -\item[node] その名の通り node に格納されている値を保存する。 色と値となる自然数が入る -\item[tree] tree の構造 を保存する。ここで node と x / right tree を持つ -\item[rbt] 上3つの要素を合わせて持つことで Left Learning Red Black Tree を定義する -\item[Env] rbt 以外に追加や削除を行う対象となる値と、 rbtを保存できる List を持つ Data Gear -\end{description} + +\begin{itemize} +\item col: 色のことで、red と black の data 型で記述し、パターンマッチを行う。 +\item node: その名の通り node に格納されている値を保存する。 色と自然数が入る +\item tree: tree の構造 を保存する。ここで node と x / right tree を持つ +\item rbt: 上3つの要素を合わせて持つことで Left Learning Red Black Tree を定義する +\item Env: rbt 以外に追加や削除を行う対象となる値と、 rbtを保存できる List を持つ Data Gear +\end{itemize} \subsection{目的の node まで辿る Gears Agda} 上記に示した手順通りにAgdaで記述すると下 \coderef{insert_imple}のようになる。
--- a/paper/tex/rbt_verif.tex Mon Feb 15 21:42:10 2021 +0900 +++ b/paper/tex/rbt_verif.tex Mon Feb 15 23:36:39 2021 +0900 @@ -1,5 +1,6 @@ -\chapter{Red Black Tree の検証} -実装が困難であったため、検証するまでには至らなかった。 +\chapter{Left Learning Red Black Tree の検証} +本章では、Left Learning Red Black Tree の +検証方法について述べる \section{Meta Data Gearの記述} 検証するにあたり、Meta Deta Gear を作成し Pre / Post Condition と @@ -46,13 +47,14 @@ inserする際は値とその証明の両方を持つ事で 証明付き Data 構造を 持った List となっている。 +これを Left Learning Red Black Tree の 仕様を満たすように、 +全てに対して行う。 +その後、条件が接続されているのかを検証したのち、健全性について示す事で +Hoare Logic による検証ができる。 -以上を用いて Meta Data Gear を作成する Gears Agda は以下になる。 -これを用いることで、各 node より上の node の大小関係を検証できると考えた。 - %\subsection{Black node の数え上げ} %他にも、Left Learning Red Brack Tree の black node の数え上げを記述した。
--- a/paper/tex/thanks.tex Mon Feb 15 21:42:10 2021 +0900 +++ b/paper/tex/thanks.tex Mon Feb 15 23:36:39 2021 +0900 @@ -1,6 +1,12 @@ \chapter*{謝辞} -感謝します。 +本研究の水光、本論文の作成にあたり、御多忙にも関わらず終始懇切丁寧なる御指導と御教授 +を賜わりました、河野真治准教授に心より感謝致します。そして、 共に研究を行い暖か +な気遣いと励ましをもって支えてくれた並列信頼研究室の全てのメンバーに感謝致しま +す。また、全員最終学年であるにもかかわらず、本コースのシステム更新に関わったシス +テム管理チームに感謝いたします。 +最後に、 有意義な時間を共に過ごした理工学研究科情報工学専攻の学友、 +並びに物心両面で支えてくれた家族に深く感謝致します。 \thispagestyle{empty}
--- a/slide/slide.html Mon Feb 15 21:42:10 2021 +0900 +++ b/slide/slide.html Mon Feb 15 23:36:39 2021 +0900 @@ -1,4 +1,4 @@ -<!DOCTYPE html><html lang="ja-JP"><head><title>コンテナ技術を用いた教育情報システムの構築</title><meta property="og:title" content="コンテナ技術を用いた教育情報システムの構築"><meta charset="UTF-8"><meta name="viewport" content="width=device-width,height=device-height,initial-scale=1.0"><meta name="apple-mobile-web-app-capable" content="yes"><meta http-equiv="X-UA-Compatible" content="ie=edge"><meta property="og:type" content="website"><meta name="twitter:card" content="summary"><style>.bespoke-marp-note,.bespoke-marp-osc,.bespoke-progress-parent{display:none;transition:none}@media screen{body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button{-webkit-appearance:none;-moz-appearance:none;appearance:none;background-color:transparent;border:0;color:inherit;cursor:pointer;font-size:inherit;opacity:.8;outline:none;padding:0;transition:opacity .2s linear;-webkit-tap-highlight-color:transparent}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:disabled,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:disabled,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:disabled{cursor:not-allowed;opacity:.15!important}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:hover,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:hover,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:hover{opacity:1}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:active,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:active,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:hover:active{opacity:.6}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:not(:disabled),body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:not(:disabled),body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:hover:not(:disabled){transition:none}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev],body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button.bespoke-marp-presenter-info-page-prev{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48cGF0aCBmaWxsPSJub25lIiBzdHJva2U9IiNmZmYiIHN0cm9rZS1saW5lY2FwPSJyb3VuZCIgc3Ryb2tlLWxpbmVqb2luPSJyb3VuZCIgc3Ryb2tlLXdpZHRoPSI1IiBkPSJNNjggOTBMMjggNTBsNDAtNDAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button.bespoke-marp-presenter-info-page-next{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48cGF0aCBmaWxsPSJub25lIiBzdHJva2U9IiNmZmYiIHN0cm9rZS1saW5lY2FwPSJyb3VuZCIgc3Ryb2tlLWxpbmVqb2luPSJyb3VuZCIgc3Ryb2tlLXdpZHRoPSI1IiBkPSJNMzIgOTBsNDAtNDAtNDAtNDAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen]{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48ZGVmcz48c3R5bGU+LmF7ZmlsbDpub25lO3N0cm9rZTojZmZmO3N0cm9rZS1saW5lY2FwOnJvdW5kO3N0cm9rZS1saW5lam9pbjpyb3VuZDtzdHJva2Utd2lkdGg6NXB4fTwvc3R5bGU+PC9kZWZzPjxyZWN0IGNsYXNzPSJhIiB4PSIxMCIgeT0iMjAiIHdpZHRoPSI4MCIgaGVpZ2h0PSI2MCIgcng9IjUuNjciLz48cGF0aCBjbGFzcz0iYSIgZD0iTTQwIDcwSDIwVjUwbTIwIDBMMjAgNzBtNDAtNDBoMjB2MjBtLTIwIDBsMjAtMjAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button.exit[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button.exit[data-bespoke-marp-osc=fullscreen]{background-image:url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48ZGVmcz48c3R5bGU+LmF7ZmlsbDpub25lO3N0cm9rZTojZmZmO3N0cm9rZS1saW5lY2FwOnJvdW5kO3N0cm9rZS1saW5lam9pbjpyb3VuZDtzdHJva2Utd2lkdGg6NXB4fTwvc3R5bGU+PC9kZWZzPjxyZWN0IGNsYXNzPSJhIiB4PSIxMCIgeT0iMjAiIHdpZHRoPSI4MCIgaGVpZ2h0PSI2MCIgcng9IjUuNjciLz48cGF0aCBjbGFzcz0iYSIgZD0iTTIwIDUwaDIwdjIwbS0yMCAwbDIwLTIwbTQwIDBINjBWMzBtMjAgMEw2MCA1MCIvPjwvc3ZnPg==")}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter]{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48ZGVmcz48c3R5bGU+LmF7ZmlsbDpub25lO3N0cm9rZTojZmZmO3N0cm9rZS1saW5lY2FwOnJvdW5kO3N0cm9rZS13aWR0aDo1cHh9PC9zdHlsZT48L2RlZnM+PHBhdGggY2xhc3M9ImEiIGQ9Ik0yMCA2MGgtNWE1IDUgMCAwMS01LTVWMjBhNSA1IDAgMDE1LTVoNjBhNSA1IDAgMDE1IDV2NU0zMCA4NWg2MCIvPjxyZWN0IHg9IjMwIiB5PSIzNSIgd2lkdGg9IjYwIiBoZWlnaHQ9IjQwIiByeD0iNSIgZmlsbD0ibm9uZSIgc3Ryb2tlPSIjZmZmIi8+PHJlY3QgY2xhc3M9ImEiIHg9IjMwIiB5PSIzNSIgd2lkdGg9IjYwIiBoZWlnaHQ9IjQwIiByeD0iNSIvPjxwYXRoIGNsYXNzPSJhIiBkPSJNNDAgNTBoNDBNNDAgNjBoMzAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body,html{height:100%;margin:0}body{background:#000;overflow:hidden}svg.bespoke-marp-slide{content-visibility:hidden;z-index:-1;pointer-events:none;opacity:0}svg.bespoke-marp-slide.bespoke-marp-active{content-visibility:visible;z-index:0;pointer-events:auto;opacity:1}svg.bespoke-marp-slide.bespoke-marp-active.bespoke-marp-active-ready *{-webkit-animation-name:__bespoke_marp__!important;animation-name:__bespoke_marp__!important}@supports not (content-visibility:hidden){svg.bespoke-marp-slide[data-bespoke-marp-load=hideable]{display:none}svg.bespoke-marp-slide[data-bespoke-marp-load=hideable].bespoke-marp-active{display:block}}[data-bespoke-marp-fragment=inactive]{visibility:hidden}body[data-bespoke-view=""] .bespoke-marp-parent,body[data-bespoke-view=next] .bespoke-marp-parent{bottom:0;left:0;position:absolute;right:0;top:0}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc{background:rgba(0,0,0,.65);border-radius:7px;bottom:50px;color:#fff;display:block;font-family:Helvetica,Arial,sans-serif;font-size:16px;left:50%;line-height:0;opacity:1;padding:12px;position:absolute;touch-action:manipulation;transform:translateX(-50%);transition:opacity .2s linear;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none;white-space:nowrap;z-index:1;will-change:transform}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>*,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>*{margin-left:6px}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>:first-child,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>:first-child{margin-left:0}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>span,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>span{opacity:.8}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>span[data-bespoke-marp-osc=page],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>span[data-bespoke-marp-osc=page]{display:inline-block;min-width:140px;text-align:center}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter],body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev]{height:32px;line-height:32px;width:32px}body[data-bespoke-view=""] .bespoke-marp-parent.bespoke-marp-inactive,body[data-bespoke-view=next] .bespoke-marp-parent.bespoke-marp-inactive{cursor:none}body[data-bespoke-view=""] .bespoke-marp-parent.bespoke-marp-inactive>.bespoke-marp-osc,body[data-bespoke-view=next] .bespoke-marp-parent.bespoke-marp-inactive>.bespoke-marp-osc{opacity:0;pointer-events:none}body[data-bespoke-view=""] svg.bespoke-marp-slide,body[data-bespoke-view=next] svg.bespoke-marp-slide{height:100%;left:0;position:absolute;top:0;width:100%}body[data-bespoke-view=""] .bespoke-progress-parent{background:#222;display:flex;height:5px;width:100%}body[data-bespoke-view=""] .bespoke-progress-parent+.bespoke-marp-parent{top:5px}body[data-bespoke-view=""] .bespoke-progress-parent .bespoke-progress-bar{flex:0 0 0;background:#0288d1;transition:flex-basis .2s cubic-bezier(0,1,1,1)}body[data-bespoke-view=next]{background:transparent}body[data-bespoke-view=presenter]{background:#161616}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container{font-family:Helvetica,Arial,sans-serif;height:100%;left:0;position:absolute;top:0;width:100%;display:grid;grid-template-columns:2fr 1fr;grid-template-rows:minmax(140px,1fr) 2fr 3em;grid-template-areas:"current next" "current note" "info note"}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-parent{grid-area:current;position:relative;overflow:hidden}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-parent svg.bespoke-marp-slide{height:calc(100% - 40px);left:20px;position:absolute;pointer-events:none;top:20px;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none;width:calc(100% - 40px)}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-parent svg.bespoke-marp-slide.bespoke-marp-active{filter:drop-shadow(0 3px 10px rgba(0,0,0,.5))}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-next-container{background:#222;cursor:pointer;display:none;grid-area:next;overflow:hidden;position:relative}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-next-container.active{display:block}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-next-container iframe.bespoke-marp-presenter-next{background:transparent;border:0;display:block;filter:drop-shadow(0 3px 10px rgba(0,0,0,.5));height:calc(100% - 40px);left:20px;position:absolute;pointer-events:none;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none;top:20px;width:calc(100% - 40px)}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container{background:#222;color:#eee;grid-area:note}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note{margin:20px;width:calc(100% - 40px);height:calc(100% - 40px);box-sizing:border-box;font-size:1.1em;overflow:auto;padding-right:3px;white-space:pre-wrap;word-wrap:break-word;scrollbar-width:thin;scrollbar-color:hsla(0,0%,93.3%,.5) transparent}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note::-webkit-scrollbar{width:6px}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note::-webkit-scrollbar-track{background:transparent}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note::-webkit-scrollbar-thumb{background:hsla(0,0%,93.3%,.5);border-radius:6px}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note:empty{pointer-events:none}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note.active{display:block}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note p:first-child{margin-top:0}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note p:last-child{margin-bottom:0}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container{align-items:center;box-sizing:border-box;color:#eee;display:flex;flex-wrap:nowrap;grid-area:info;justify-content:center;padding:0 10px}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-page,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-time,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-timer{display:block;box-sizing:border-box;padding:0 10px;white-space:nowrap;width:100%}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button{height:1.5em;line-height:1.5em;width:1.5em}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-page{order:2;text-align:center}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-page .bespoke-marp-presenter-info-page-text{display:inline-block;min-width:120px;text-align:center}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-time{color:#999;order:1;text-align:left}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-timer{color:#999;order:3;text-align:right}}@media print{.bespoke-marp-presenter-info-container,.bespoke-marp-presenter-next-container,.bespoke-marp-presenter-note-container{display:none}}</style><style>div#p>svg>foreignObject>section{width:1280px;height:720px;box-sizing:border-box;overflow:hidden;position:relative;scroll-snap-align:center center}div#p>svg>foreignObject>section:after{bottom:0;content:attr(data-marpit-pagination);padding:inherit;pointer-events:none;position:absolute;right:0}div#p>svg>foreignObject>section:not([data-marpit-pagination]):after{display:none}/* Normalization */div#p>svg>foreignObject>section h1{font-size:2em;margin:0.67em 0}div#p>svg>foreignObject>section video::-webkit-media-controls{will-change:transform}@page{size:1280px 720px;margin:0}@media print{body,html{background-color:#fff;margin:0;page-break-inside:avoid;break-inside:avoid-page}div#p>svg>foreignObject>section{page-break-before:always;break-before:page}div#p>svg>foreignObject>section,div#p>svg>foreignObject>section *{-webkit-print-color-adjust:exact!important;animation-delay:0s!important;animation-duration:0s!important;color-adjust:exact!important;transition:none!important}div#p>svg[data-marpit-svg]{display:block;height:100vh;width:100vw}}div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{display:block;height:auto;width:100%}@supports (-ms-ime-align:auto){div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{position:static}}div#p>svg>foreignObject>section svg[data-marp-fitting=svg].__reflow__{content:""}@supports (-ms-ime-align:auto){div#p>svg>foreignObject>section svg[data-marp-fitting=svg].__reflow__{position:relative}}div#p>svg>foreignObject>section [data-marp-fitting-svg-content]{display:table;white-space:nowrap}div#p>svg>foreignObject>section [data-marp-fitting-svg-content-wrap]{white-space:pre}div#p>svg>foreignObject>section img[data-marp-twemoji]{background:transparent;height:1em;margin:0 .05em 0 .1em;vertical-align:-.1em;width:1em} +<!DOCTYPE html><html lang="ja-JP"><head><title>Geas Agda による Left Learning Red Black Tree の検証</title><meta property="og:title" content="Geas Agda による Left Learning Red Black Tree の検証"><meta charset="UTF-8"><meta name="viewport" content="width=device-width,height=device-height,initial-scale=1.0"><meta name="apple-mobile-web-app-capable" content="yes"><meta http-equiv="X-UA-Compatible" content="ie=edge"><meta property="og:type" content="website"><meta name="twitter:card" content="summary"><style>.bespoke-marp-note,.bespoke-marp-osc,.bespoke-progress-parent{display:none;transition:none}@media screen{body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button{-webkit-appearance:none;-moz-appearance:none;appearance:none;background-color:transparent;border:0;color:inherit;cursor:pointer;font-size:inherit;opacity:.8;outline:none;padding:0;transition:opacity .2s linear;-webkit-tap-highlight-color:transparent}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:disabled,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:disabled,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:disabled{cursor:not-allowed;opacity:.15!important}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:hover,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:hover,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:hover{opacity:1}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:active,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:active,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:hover:active{opacity:.6}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:not(:disabled),body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:not(:disabled),body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:hover:not(:disabled){transition:none}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev],body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button.bespoke-marp-presenter-info-page-prev{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48cGF0aCBmaWxsPSJub25lIiBzdHJva2U9IiNmZmYiIHN0cm9rZS1saW5lY2FwPSJyb3VuZCIgc3Ryb2tlLWxpbmVqb2luPSJyb3VuZCIgc3Ryb2tlLXdpZHRoPSI1IiBkPSJNNjggOTBMMjggNTBsNDAtNDAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button.bespoke-marp-presenter-info-page-next{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48cGF0aCBmaWxsPSJub25lIiBzdHJva2U9IiNmZmYiIHN0cm9rZS1saW5lY2FwPSJyb3VuZCIgc3Ryb2tlLWxpbmVqb2luPSJyb3VuZCIgc3Ryb2tlLXdpZHRoPSI1IiBkPSJNMzIgOTBsNDAtNDAtNDAtNDAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen]{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48ZGVmcz48c3R5bGU+LmF7ZmlsbDpub25lO3N0cm9rZTojZmZmO3N0cm9rZS1saW5lY2FwOnJvdW5kO3N0cm9rZS1saW5lam9pbjpyb3VuZDtzdHJva2Utd2lkdGg6NXB4fTwvc3R5bGU+PC9kZWZzPjxyZWN0IGNsYXNzPSJhIiB4PSIxMCIgeT0iMjAiIHdpZHRoPSI4MCIgaGVpZ2h0PSI2MCIgcng9IjUuNjciLz48cGF0aCBjbGFzcz0iYSIgZD0iTTQwIDcwSDIwVjUwbTIwIDBMMjAgNzBtNDAtNDBoMjB2MjBtLTIwIDBsMjAtMjAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button.exit[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button.exit[data-bespoke-marp-osc=fullscreen]{background-image:url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48ZGVmcz48c3R5bGU+LmF7ZmlsbDpub25lO3N0cm9rZTojZmZmO3N0cm9rZS1saW5lY2FwOnJvdW5kO3N0cm9rZS1saW5lam9pbjpyb3VuZDtzdHJva2Utd2lkdGg6NXB4fTwvc3R5bGU+PC9kZWZzPjxyZWN0IGNsYXNzPSJhIiB4PSIxMCIgeT0iMjAiIHdpZHRoPSI4MCIgaGVpZ2h0PSI2MCIgcng9IjUuNjciLz48cGF0aCBjbGFzcz0iYSIgZD0iTTIwIDUwaDIwdjIwbS0yMCAwbDIwLTIwbTQwIDBINjBWMzBtMjAgMEw2MCA1MCIvPjwvc3ZnPg==")}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter]{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48ZGVmcz48c3R5bGU+LmF7ZmlsbDpub25lO3N0cm9rZTojZmZmO3N0cm9rZS1saW5lY2FwOnJvdW5kO3N0cm9rZS13aWR0aDo1cHh9PC9zdHlsZT48L2RlZnM+PHBhdGggY2xhc3M9ImEiIGQ9Ik0yMCA2MGgtNWE1IDUgMCAwMS01LTVWMjBhNSA1IDAgMDE1LTVoNjBhNSA1IDAgMDE1IDV2NU0zMCA4NWg2MCIvPjxyZWN0IHg9IjMwIiB5PSIzNSIgd2lkdGg9IjYwIiBoZWlnaHQ9IjQwIiByeD0iNSIgZmlsbD0ibm9uZSIgc3Ryb2tlPSIjZmZmIi8+PHJlY3QgY2xhc3M9ImEiIHg9IjMwIiB5PSIzNSIgd2lkdGg9IjYwIiBoZWlnaHQ9IjQwIiByeD0iNSIvPjxwYXRoIGNsYXNzPSJhIiBkPSJNNDAgNTBoNDBNNDAgNjBoMzAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body,html{height:100%;margin:0}body{background:#000;overflow:hidden}svg.bespoke-marp-slide{content-visibility:hidden;z-index:-1;pointer-events:none;opacity:0}svg.bespoke-marp-slide.bespoke-marp-active{content-visibility:visible;z-index:0;pointer-events:auto;opacity:1}svg.bespoke-marp-slide.bespoke-marp-active.bespoke-marp-active-ready *{-webkit-animation-name:__bespoke_marp__!important;animation-name:__bespoke_marp__!important}@supports not (content-visibility:hidden){svg.bespoke-marp-slide[data-bespoke-marp-load=hideable]{display:none}svg.bespoke-marp-slide[data-bespoke-marp-load=hideable].bespoke-marp-active{display:block}}[data-bespoke-marp-fragment=inactive]{visibility:hidden}body[data-bespoke-view=""] .bespoke-marp-parent,body[data-bespoke-view=next] .bespoke-marp-parent{bottom:0;left:0;position:absolute;right:0;top:0}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc{background:rgba(0,0,0,.65);border-radius:7px;bottom:50px;color:#fff;display:block;font-family:Helvetica,Arial,sans-serif;font-size:16px;left:50%;line-height:0;opacity:1;padding:12px;position:absolute;touch-action:manipulation;transform:translateX(-50%);transition:opacity .2s linear;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none;white-space:nowrap;z-index:1;will-change:transform}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>*,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>*{margin-left:6px}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>:first-child,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>:first-child{margin-left:0}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>span,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>span{opacity:.8}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>span[data-bespoke-marp-osc=page],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>span[data-bespoke-marp-osc=page]{display:inline-block;min-width:140px;text-align:center}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter],body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev]{height:32px;line-height:32px;width:32px}body[data-bespoke-view=""] .bespoke-marp-parent.bespoke-marp-inactive,body[data-bespoke-view=next] .bespoke-marp-parent.bespoke-marp-inactive{cursor:none}body[data-bespoke-view=""] .bespoke-marp-parent.bespoke-marp-inactive>.bespoke-marp-osc,body[data-bespoke-view=next] .bespoke-marp-parent.bespoke-marp-inactive>.bespoke-marp-osc{opacity:0;pointer-events:none}body[data-bespoke-view=""] svg.bespoke-marp-slide,body[data-bespoke-view=next] svg.bespoke-marp-slide{height:100%;left:0;position:absolute;top:0;width:100%}body[data-bespoke-view=""] .bespoke-progress-parent{background:#222;display:flex;height:5px;width:100%}body[data-bespoke-view=""] .bespoke-progress-parent+.bespoke-marp-parent{top:5px}body[data-bespoke-view=""] .bespoke-progress-parent .bespoke-progress-bar{flex:0 0 0;background:#0288d1;transition:flex-basis .2s cubic-bezier(0,1,1,1)}body[data-bespoke-view=next]{background:transparent}body[data-bespoke-view=presenter]{background:#161616}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container{font-family:Helvetica,Arial,sans-serif;height:100%;left:0;position:absolute;top:0;width:100%;display:grid;grid-template-columns:2fr 1fr;grid-template-rows:minmax(140px,1fr) 2fr 3em;grid-template-areas:"current next" "current note" "info note"}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-parent{grid-area:current;position:relative;overflow:hidden}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-parent svg.bespoke-marp-slide{height:calc(100% - 40px);left:20px;position:absolute;pointer-events:none;top:20px;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none;width:calc(100% - 40px)}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-parent svg.bespoke-marp-slide.bespoke-marp-active{filter:drop-shadow(0 3px 10px rgba(0,0,0,.5))}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-next-container{background:#222;cursor:pointer;display:none;grid-area:next;overflow:hidden;position:relative}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-next-container.active{display:block}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-next-container iframe.bespoke-marp-presenter-next{background:transparent;border:0;display:block;filter:drop-shadow(0 3px 10px rgba(0,0,0,.5));height:calc(100% - 40px);left:20px;position:absolute;pointer-events:none;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none;top:20px;width:calc(100% - 40px)}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container{background:#222;color:#eee;grid-area:note}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note{margin:20px;width:calc(100% - 40px);height:calc(100% - 40px);box-sizing:border-box;font-size:1.1em;overflow:auto;padding-right:3px;white-space:pre-wrap;word-wrap:break-word;scrollbar-width:thin;scrollbar-color:hsla(0,0%,93.3%,.5) transparent}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note::-webkit-scrollbar{width:6px}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note::-webkit-scrollbar-track{background:transparent}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note::-webkit-scrollbar-thumb{background:hsla(0,0%,93.3%,.5);border-radius:6px}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note:empty{pointer-events:none}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note.active{display:block}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note p:first-child{margin-top:0}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note p:last-child{margin-bottom:0}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container{align-items:center;box-sizing:border-box;color:#eee;display:flex;flex-wrap:nowrap;grid-area:info;justify-content:center;padding:0 10px}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-page,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-time,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-timer{display:block;box-sizing:border-box;padding:0 10px;white-space:nowrap;width:100%}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button{height:1.5em;line-height:1.5em;width:1.5em}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-page{order:2;text-align:center}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-page .bespoke-marp-presenter-info-page-text{display:inline-block;min-width:120px;text-align:center}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-time{color:#999;order:1;text-align:left}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-timer{color:#999;order:3;text-align:right}}@media print{.bespoke-marp-presenter-info-container,.bespoke-marp-presenter-next-container,.bespoke-marp-presenter-note-container{display:none}}</style><style>div#p>svg>foreignObject>section{width:1280px;height:720px;box-sizing:border-box;overflow:hidden;position:relative;scroll-snap-align:center center}div#p>svg>foreignObject>section:after{bottom:0;content:attr(data-marpit-pagination);padding:inherit;pointer-events:none;position:absolute;right:0}div#p>svg>foreignObject>section:not([data-marpit-pagination]):after{display:none}/* Normalization */div#p>svg>foreignObject>section h1{font-size:2em;margin:0.67em 0}div#p>svg>foreignObject>section video::-webkit-media-controls{will-change:transform}@page{size:1280px 720px;margin:0}@media print{body,html{background-color:#fff;margin:0;page-break-inside:avoid;break-inside:avoid-page}div#p>svg>foreignObject>section{page-break-before:always;break-before:page}div#p>svg>foreignObject>section,div#p>svg>foreignObject>section *{-webkit-print-color-adjust:exact!important;animation-delay:0s!important;animation-duration:0s!important;color-adjust:exact!important;transition:none!important}div#p>svg[data-marpit-svg]{display:block;height:100vh;width:100vw}}div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{display:block;height:auto;width:100%}@supports (-ms-ime-align:auto){div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{position:static}}div#p>svg>foreignObject>section svg[data-marp-fitting=svg].__reflow__{content:""}@supports (-ms-ime-align:auto){div#p>svg>foreignObject>section svg[data-marp-fitting=svg].__reflow__{position:relative}}div#p>svg>foreignObject>section [data-marp-fitting-svg-content]{display:table;white-space:nowrap}div#p>svg>foreignObject>section [data-marp-fitting-svg-content-wrap]{white-space:pre}div#p>svg>foreignObject>section img[data-marp-twemoji]{background:transparent;height:1em;margin:0 .05em 0 .1em;vertical-align:-.1em;width:1em} /*! * Marp default theme. * @@ -27,11 +27,11 @@ position: absolute; left: 50px; top: 35px; } -" class="title" data-marpit-pagination="1" data-marpit-pagination-total="32" style="--paginate:true;--class:title;--theme:default; +" class="title" data-marpit-pagination="1" data-marpit-pagination-total="11" style="--paginate:true;--class:title;--theme:default; ;"> -<h1><svg data-marp-fitting="svg"><foreignObject><span data-marp-fitting-svg-content> コンテナ技術を用いた教育情報システムの構築</span></foreignObject></svg></h1> +<h1>Gears Agda による <br /> Left Learning Red Black Tree の検証</h1> <ul> -<li>宮平 賢 +<li>上地 悠斗 <ul> <li>琉球大学工学部工学科知能情報コース</li> </ul> @@ -62,21 +62,23 @@ position: absolute; left: 50px; top: 35px; } -" class="slide" data-marpit-pagination="2" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; +" class="slide" data-marpit-pagination="2" data-marpit-pagination-total="11" style="--paginate:true;--class:slide;--theme:default; ;"> -<h1>研究目的</h1> +<h1>証明を用いてプログラムの信頼性の向上を目指す</h1> + <ul> -<li>情報通信技術の普及に伴い学ぶことが増えている</li> -<li>その学習環境として、Virtual MachineやContainerがある +<li>プログラムの信頼性を高めることは重要な課題である <ul> -<li>高性能なPC</li> -<li>クラウドサービス -<ul> -<li>無料だと制限がある</li> +<li>信頼性を高める手法として「モデル検査」や「定理証明」など</li> </ul> </li> +<li>当研究室でCbCという言語を開発している +<ul> +<li>C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる</li> </ul> </li> +<li>先行研究では Hoare Logic を用いて 簡単なプログラムの検証を行った</li> +<li>本研究では Gears Agda にて 重要なアルゴリズムの一つである Red Black Tree を検証する</li> </ul> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="3" data-paginate="true" data-class="slide" data-theme="default" data-style="section { @@ -98,33 +100,13 @@ position: absolute; left: 50px; top: 35px; } -" class="slide" data-marpit-pagination="3" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; +" class="slide" data-marpit-pagination="3" data-marpit-pagination-total="11" style="--paginate:true;--class:slide;--theme:default; ;"> -<h1>これまでの学生向け学習環境</h1> -<ul> -<li> -<p>VM貸出サービス</p> -<ul> -<li>Akatsuki -<ul> -<li>申請を行い、Webコントロールパネルから作成</li> -</ul> -</li> -<li>ie-virsh +<h1>これまでの成果</h1> <ul> -<li>手元のPCで作成したVMイメージのデプロイ</li> -</ul> -</li> -</ul> -</li> -<li> -<p>VM貸出サービスのデフォルトスペック</p> -<ul> -<li>CPU 1コア</li> -<li>メモリ 1GB</li> -<li>ディスク容量 10GB</li> -</ul> -</li> +<li>Gears Agda</li> +<li>Gears Agda による Hoare Logic を用いた簡単なプログラムの検証</li> +<li>Gears Agda で実装したRed Black Tree(insert)</li> </ul> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="4" data-paginate="true" data-class="slide" data-theme="default" data-style="section { @@ -146,22 +128,15 @@ position: absolute; left: 50px; top: 35px; } -" class="slide" data-marpit-pagination="4" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; +" class="slide" data-marpit-pagination="4" data-marpit-pagination-total="11" style="--paginate:true;--class:slide;--theme:default; ;"> -<h1>これまでの学習環境の問題点</h1> +<h1>今回の成果</h1> <ul> -<li>VM貸出サービスの一部学生は申請の方法が分からなかったり、貸出サービスがあることが周知されていなかったため、旧システムのリソースが余っていた</li> -</ul> -<br /> -<ul> -<li>VMのスペックの変更にはシステム管理チームへの申請が必要であり、利用者と管理者とのやり取りなどの手間があった</li> -</ul> -<br /> -<ul> -<li>旧システムにはGPUが搭載されていないため、貸出サービスではなく研究室ごとの機器、クラウドサービスが多く利用された</li> +<li>Left Lerning Red Black Tree の実装</li> +<li>証明付き Data 構造を用いた List による性質の記述</li> </ul> </section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="5" data-paginate="true" data-class="title" data-theme="default" data-style="section { +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="5" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -180,9 +155,22 @@ position: absolute; left: 50px; top: 35px; } -" class="title" data-marpit-pagination="5" data-marpit-pagination-total="32" style="--paginate:true;--class:title;--theme:default; +" class="slide" data-marpit-pagination="5" data-marpit-pagination-total="11" style="--paginate:true;--class:slide;--theme:default; ;"> -<h1>教育情報システムの構築</h1> +<h1>Left Learning Red Black Tree</h1> +<ul> +<li>Red Black Tree の定義を満たしつつ、実装が容易な Binary Treeの一つ</li> +<li>insert / delete / search の最悪実行時間がlog nである重要なアルゴリズム</li> +<li>定義は以下となる +<ul> +<li>各点は赤か黒の色である</li> +<li>点が赤である場合の親となる点の色は黒である</li> +<li>外点 (葉。つまり一番下の点) は黒である</li> +<li>任意の点から外点までの黒色の点はいずれも同数となる。</li> +<li>node は parent から見て左の node にしか 現れない</li> +</ul> +</li> +</ul> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -203,43 +191,10 @@ position: absolute; left: 50px; top: 35px; } -" class="slide" data-marpit-pagination="6" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; +" class="slide" data-marpit-pagination="6" data-marpit-pagination-total="11" style="--paginate:true;--class:slide;--theme:default; ;"> -<h1>オンプレミス環境</h1> -<ul> -<li>汎用サーバ x 4</li> -<li>ディスクサーバ x 2</li> -</ul> -<table> -<thead> -<tr> -<th style="text-align:center"></th> -<th style="text-align:center"></th> -</tr> -</thead> -<tbody> -<tr> -<td style="text-align:center">CPU</td> -<td style="text-align:center">Intel Xeon Gold 6238 (2.10GHz/22Core)</td> -</tr> -<tr> -<td style="text-align:center">GPU</td> -<td style="text-align:center">Nvidia Tesla V100S</td> -</tr> -<tr> -<td style="text-align:center">メモリ</td> -<td style="text-align:center">512GB</td> -</tr> -<tr> -<td style="text-align:center">SAS SSD</td> -<td style="text-align:center">5TB</td> -</tr> -<tr> -<td style="text-align:center">NVMe SSD</td> -<td style="text-align:center">1.5TB</td> -</tr> -</tbody> -</table> +<h1>Left Learning Red Black Tree の一例</h1> +<p><img src="images/llrbt.svg" alt="height:500" style="height:500px;" /></p> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="7" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -260,25 +215,15 @@ position: absolute; left: 50px; top: 35px; } -" class="slide" data-marpit-pagination="7" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; +" class="slide" data-marpit-pagination="7" data-marpit-pagination-total="11" style="--paginate:true;--class:slide;--theme:default; ;"> -<h1>VM貸出サービスの移行</h1> -<ul> -<li>VM貸出サービスを継続するため、KVMを導入する</li> -<li>VMからGPUの利用にはPCIパススルーの設定が必要となる</li> -<li>しかし、VM1つに対し、1つのGPUが必要になる +<h1>Gears Agda による Left Leaning Red Black Tree の記述</h1> <ul> -<li>希望する学生全員に割り当てができない</li> -</ul> -</li> -</ul> -<br /> -<ul> -<li>そこで、コンテナ環境を導入する -<ul> -<li>1つのGPUを複数のコンテナから利用できる</li> -</ul> -</li> +<li>通常のプログラミング言語であれば、再代入と再帰処理を用いて実装を行う</li> +<li>Gears Agda では両方行えないため、これらを回避する</li> +<li>insert / delete をする際に、目的の node まで辿るが、ここで辿った分を<br /> +Listに保持する</li> +<li>目的の node まで辿った後に、List に保持した node を結合させることで実装を行う</li> </ul> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="8" data-paginate="true" data-class="slide" data-theme="default" data-style="section { @@ -300,29 +245,23 @@ position: absolute; left: 50px; top: 35px; } -" class="slide" data-marpit-pagination="8" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; +" class="slide" data-marpit-pagination="8" data-marpit-pagination-total="11" style="--paginate:true;--class:slide;--theme:default; ;"> -<h1>コンテナ環境の導入</h1> -<ul> -<li>要件としてマルチユーザであり、GPUが利用できるなどがある</li> -<li>そこで、Podman、Singularityを導入する</li> -<li>Podman -<ul> -<li>rootlessで利用できる</li> -<li>nvidia-dockerの設定を行えばGPUを利用できる</li> -</ul> -</li> -<li>Singularity -<ul> -<li>rootlessで利用できる</li> -<li>GPUの利用が容易 -<ul> -<li>GPUドライバーのインストールのみ</li> -</ul> -</li> -</ul> -</li> -</ul> +<h1>実際の Left Leaning Red Black Tree の実装コード</h1> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>insert-c : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +insert-c env next exit with Env.vart env +... | bt-empty = exit record env{vart = (bt-node (record { + key = record { coler = red ; number = Env.varn env }; + ltree = bt-empty; rtree = bt-empty }))} +... | bt-node node with <-cmp (Env.varn env) (node.number (tree.key node)) +... | tri≈ ¬a b ¬c = exit env +... | tri> ¬a ¬b c = next record env{ + vart = (tree.ltree node) ; + varl = (bt-node record node{ltree = bt-empty}) ∷ (Env.varl env) } +... | tri< a ¬b ¬c = next record env{ + vart = (tree.rtree node) ; + varl = (bt-node record node{rtree = bt-empty}) ∷ (Env.varl env) } +</span></span></foreignObject></svg></code></pre> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="9" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -343,39 +282,19 @@ position: absolute; left: 50px; top: 35px; } -" class="slide" data-marpit-pagination="9" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; +" class="slide" data-marpit-pagination="9" data-marpit-pagination-total="11" style="--paginate:true;--class:slide;--theme:default; ;"> -<h1>コンテナエンジンの補い</h1> -<ul> -<li> -<p>Podman</p> +<h1>証明付き Data 構造を用いた List による性質の記述</h1> <ul> -<li>イメージの作成やコンテナの作成が遅い -<ul> -<li>Podmanがまだ開発段階</li> -</ul> -</li> -<li>rootlessでは実行できない機能がある -<ul> -<li>IPアドレスの割り当て</li> +<li>検証には実装が仕様を満たしている必要がある</li> +<li>Binary Tree の性質も持っているので、大小関係を検証する</li> +<li>そこで、証明付き Data 構造を用いた List を下記のように定義した</li> </ul> -</li> -</ul> -</li> -<li> -<p>Singularity</p> -<ul> -<li>イメージの作成に時間がかかる -<ul> -<li>ビルド中にエラーが発生すると、一から再開する必要がある</li> -</ul> -</li> -</ul> -</li> -<li> -<p>そこでPodmanのwrapperであるie-podmanを作成した</p> -</li> -</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>data right-List : Set where + [] : right-List + [_] : ℕ → right-List + _∷>_Cond_ : (x : ℕ) → (xs : right-List ) → (p : x Data.Nat.> top-r xs) → right-List +</span></span></foreignObject></svg></code></pre> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -396,16 +315,17 @@ position: absolute; left: 50px; top: 35px; } -" class="slide" data-marpit-pagination="10" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; +" class="slide" data-marpit-pagination="10" data-marpit-pagination-total="11" style="--paginate:true;--class:slide;--theme:default; ;"> -<h1>ie-podmanの作成</h1> +<h1>今後の課題</h1> <ul> -<li>ユーザのUID、GIDを取得し管理を行う +<li>作成した Left Learning Red Black Tree を Hoare Logicに当てはめる</li> +<li>その後、条件の接続ができているのかと、健全性について示す</li> +<li>CbCはC言語とアセンブラの中間言語に位置しており、人が書くのは困難である <ul> -<li>他のユーザのリソースを操作できない</li> +<li>そのため、Gears Agda から CbC へ変換ができないか調査する</li> </ul> </li> -<li>SSD上にイメージ等を保存し、高速を図る</li> </ul> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-class="slide" data-theme="default" data-style="section { @@ -427,853 +347,27 @@ position: absolute; left: 50px; top: 35px; } -" class="slide" data-marpit-pagination="11" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; +" class="slide" data-marpit-pagination="11" data-marpit-pagination-total="11" style="--paginate:true;--class:slide;--theme:default; ;"> -<h1>ie-podmanの機能 1/2</h1> -<ul> -<li>Podmanのすべての機能をwrappするのではなく、一部機能のみを提供する</li> -</ul> -<table> -<thead> -<tr> -<th>コマンド</th> -<th>機能</th> -</tr> -</thead> -<tbody> -<tr> -<td>build</td> -<td>Containerfileの指示に従いイメージを作成する</td> -</tr> -<tr> -<td>cp</td> -<td>コンテナにファイルを送信する</td> -</tr> -<tr> -<td>exec</td> -<td>起動中のコンテナでプロセスを実行する</td> -</tr> -<tr> -<td>images</td> -<td>コンテナイメージの一覧を表示する</td> -</tr> -<tr> -<td>info</td> -<td>コンテナの情報を表示する</td> -</tr> -<tr> -<td>logs</td> -<td>コンテナのlogを表示する</td> -</tr> -<tr> -<td>ps</td> -<td>起動中のコンテナの一覧を表示する</td> -</tr> -</tbody> -</table> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="12" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<h1>ie-podmanの機能 2/2</h1> +<h1>まとめ</h1> <ul> -<li>registryやsifなど独自機能を提供する</li> -</ul> -<table> -<thead> -<tr> -<th>コマンド</th> -<th>機能</th> -</tr> -</thead> -<tbody> -<tr> -<td>registry</td> -<td>学科のレジストリの操作を行う</td> -</tr> -<tr> -<td>rm</td> -<td>コンテナを削除する</td> -</tr> -<tr> -<td>run</td> -<td>コンテナを作成する</td> -</tr> -<tr> -<td>sif</td> -<td>イメージをsifファイルに変換する</td> -</tr> -<tr> -<td>start</td> -<td>コンテナを起動する</td> -</tr> -<tr> -<td>stop</td> -<td>コンテナを停止する</td> -</tr> -</tbody> -</table> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="13" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<h1>ジョブスケジューラの導入</h1> +<li>Left Learning Red Black Tree について記述した</li> +<li>Meta Data Gear を記述した <ul> -<li>多くのリソースを必要とするプログラムは管理が必要である</li> -<li>4台のサーバのリソースを利用できるようにする必要がある</li> -<li>そこで、ジョブスケジューラのSlurmを採用する -<ul> -<li>フォールトトレラントで拡張性が高い</li> -</ul> -</li> -</ul> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="14" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<h1>ジョブスケジューラの構築</h1> -<p>利用方針 <strong>「計算リソースの利用効率を上げる」</strong></p> -<ul> -<li>Jobの優先順位 -<ul> -<li>要求するリソースの少ないJobの優先度を高くする</li> -<li>実行時間が短いJobの優先度を高くする</li> -<li>これまでのJobの実行履歴で優先度は変化しない</li> -</ul> -</li> -</ul> -<p>これでは多くのリソースを要求するJobが実行されない可能性がある。</p> -<ul> -<li>Jobの実行時間 -<ul> -<li>Jobの実行時間の記載がない場合は<strong>1日で強制終了</strong>させる</li> -<li>管理者からJobの優先度を上げる</li> +<li>証明付き Data 構造を用いた List による性質の記述</li> </ul> </li> -</ul> -<p>また、Jobのスケジュールにはバックフィルを採用する。</p> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="15" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<p><img src="images/backfill.png" alt="" /></p> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="16" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<h1>ファイルシステムの導入</h1> -<ul> -<li>Cephを採用 -<ul> -<li>自己修復、自己管理機能を搭載するため信頼性が高い</li> -<li>柔軟なアクセス方法の提供 -<ul> -<li>Object Gateway</li> -<li>ブロックデバイス</li> -<li>POSIX互換のファイルシステム</li> -</ul> -</li> -</ul> -</li> -</ul> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="17" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<h1>教育情報システムの構成</h1> -<ul> -<li>汎用サーバ全てにKVM、Podman、Singularityをインストール</li> -<li>Slurm -<ul> -<li>汎用サーバ1台をコントローラ/計算ノード</li> -<li>残りを計算ノード</li> -</ul> -</li> -<li>Ceph -<ul> -<li>ディスクサーバをOSD</li> -<li>汎用サーバ3台をMON, MDS, MGR</li> -</ul> -</li> -</ul> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="18" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;" data-marpit-advanced-background="background"><div data-marpit-advanced-background-container="true" data-marpit-advanced-background-direction="horizontal"><figure style="background-image:url("images/system.png");background-size:80%;"></figure></div></section></foreignObject><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="18" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;" data-marpit-advanced-background="content"></section> -</foreignObject><foreignObject width="1280" height="720" data-marpit-advanced-background="pseudo"><section class="slide" style="" data-marpit-advanced-background="pseudo" data-marpit-pagination="18" data-marpit-pagination-total="32"></section></foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-class="title" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="title" data-marpit-pagination="19" data-marpit-pagination-total="32" style="--paginate:true;--class:title;--theme:default; -;"> -<h1>教育情報システムの利用と管理</h1> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="20" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<h1>VM貸出サービスの利用</h1> -<ul> -<li>VMの作成、スペックの変更で申請が必要なくなった</li> -<li>VMの作成 -<ul> -<li><code>ie-virsh define --template Ubuntu-20 VM_NAME</code></li> -</ul> -</li> -<li>スペックの変更 -<ul> -<li><code>ie-virsh edit VM_NAME</code></li> -</ul> -</li> -</ul> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="21" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="21" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<h1>ie-podmanの使用方法</h1> -<ul> -<li>PodmanはDockerと同じCLIを提供している</li> -<li>IPアドレス、GPUをコンテナへ割り当てられる -<ul> -<li><code>ie-podman run --ip --gpu [IMAGE_NAME]</code></li> -</ul> -</li> -<li>作成したイメージをsifファイルへの変換に対応 -<ul> -<li><code>ie-podman sif [IMAGE_NAME]</code></li> -</ul> -</li> +<li>今後検証に向けて、条件の接続と、健全性について示す</li> </ul> </section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="22" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="22" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<h1>GPUの利用方法</h1> -<ul> -<li>Singularityでは容易にGPUを利用できる -<ul> -<li><code>singularity run --nv [SIF_NAME]</code></li> -</ul> -</li> -<li>ホームディレクトリ、/tmpなどがコンテナにマウントされる -<ul> -<li>プログラムの実行に便利</li> -</ul> -</li> -<li>SlurmによるJob管理 -<ul> -<li>必要なリソースを記述し投下する</li> -<li>CPU数、GPU数</li> -</ul> -</li> -</ul> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="23" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="23" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<h1>batchファイルの例</h1> -<ul> -<li>Jobに必要とするリソース -<ul> -<li>CPU 8コア、GPU 1つ</li> -</ul> -</li> -<li>Jobの実行時間 -<ul> -<li>1分</li> -</ul> -</li> -</ul> -<pre><code class="language-bash"><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap><span class="hljs-meta">#!/bin/bash</span> -<span class="hljs-comment">#SBATCH --job-name sample</span> -<span class="hljs-comment">#SBATCH --output logs/%x-%j.log</span> -<span class="hljs-comment">#SBATCH --error logs/%x-%j.err</span> -<span class="hljs-comment">#SBATCH --nodes 1</span> -<span class="hljs-comment">#SBATCH --cpus-per-task 8</span> -<span class="hljs-comment">#SBATCH --gpus tesla:1</span> -<span class="hljs-comment">#SBATCH --time 01:00</span> - -singularity <span class="hljs-built_in">exec</span> --nv [SIF_NAME] [COMMANDS] -</span></span></foreignObject></svg></code></pre> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="24" data-paginate="true" data-class="title" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="title" data-marpit-pagination="24" data-marpit-pagination-total="32" style="--paginate:true;--class:title;--theme:default; -;"> -<h1>教育情報システムの評価</h1> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="25" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="25" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<h1>ファイルシステムの評価 1/2</h1> -<ul> -<li> -<p>実験概要</p> -<ul> -<li><code>dd</code>コマンドを使用し書き込み速度を比較する</li> -</ul> -</li> -<li> -<p>書き込み速度の比較</p> -<ul> -<li>GFS2</li> -<li>NFS</li> -<li>CephFS</li> -<li>CephRBD</li> -</ul> -</li> -</ul> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="26" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;" data-marpit-advanced-background="background"><div data-marpit-advanced-background-container="true" data-marpit-advanced-background-direction="horizontal"><figure style="background-image:url("images/fswrite.png");background-size:70%;"></figure></div></section></foreignObject><foreignObject width="1280" height="720"><section id="26" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="26" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;" data-marpit-advanced-background="content"> -<h1>ファイルシステムの評価 2/2</h1> -</section> -</foreignObject><foreignObject width="1280" height="720" data-marpit-advanced-background="pseudo"><section class="slide" style="" data-marpit-advanced-background="pseudo" data-marpit-pagination="26" data-marpit-pagination-total="32"></section></foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="27" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="27" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<h1>ie-podmanの評価 1/3</h1> -<ul> -<li> -<p>実験環境</p> -<ul> -<li>新システムの汎用サーバで実施</li> -</ul> -</li> -<li> -<p>実験概要</p> -<ul> -<li>イメージのBuild速度を比較する</li> -</ul> -</li> -<li> -<p>Build速度の比較</p> -<ul> -<li>Docker</li> -<li>Podman (rootless)</li> -<li>ie-podman</li> -</ul> -</li> -</ul> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="28" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="28" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<h1>ie-podmanの評価 2/3</h1> -<pre><code class="language-Dockerfile"><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap><span class="hljs-keyword">FROM</span> ubuntu:<span class="hljs-number">18.04</span> -<span class="hljs-keyword">RUN</span><span class="bash"> apt-get update && \ - apt-get upgrade -y && \ - DEBIAN_FRONTEND=noninteractive \ - apt-get install -y \ - qemu-utils qemu-efi-aarch64 \ - qemu-system-arm qemu-system-x86 \ - build-essential uuid-dev \ - git python iasl wget vim nasm && \ - DEBIAN_FRONTEND=noninteractive \ - apt-get install -y \ - crossbuild-essential-armhf</span> - -<span class="hljs-keyword">WORKDIR</span><span class="bash"> /workdir</span> -<span class="hljs-keyword">RUN</span><span class="bash"> git <span class="hljs-built_in">clone</span> --recursive https://github.com/tianocore/edk2 && \ - wget https://sourceforge.net/projects/gnu-efi/files/gnu-efi-3.0.12.tar.bz2/download && \ - tar xf download</span> -</span></span></foreignObject></svg></code></pre> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="29" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;" data-marpit-advanced-background="background"><div data-marpit-advanced-background-container="true" data-marpit-advanced-background-direction="horizontal"><figure style="background-image:url("images/container.png");background-size:70%;"></figure></div></section></foreignObject><foreignObject width="1280" height="720"><section id="29" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="29" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;" data-marpit-advanced-background="content"> -<h1>ie-podmanの評価 3/3</h1> -</section> -</foreignObject><foreignObject width="1280" height="720" data-marpit-advanced-background="pseudo"><section class="slide" style="" data-marpit-advanced-background="pseudo" data-marpit-pagination="29" data-marpit-pagination-total="32"></section></foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="30" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="30" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<h1>学習環境の評価</h1> -<ul> -<li>VM -<ul> -<li>学生が自由にスペックを変更できる</li> -<li>ディスク容量を抑えれる</li> -</ul> -</li> -<li>コンテナ -<ul> -<li>気軽に利用できる</li> -<li>高性能な実況環境を利用できる</li> -</ul> -</li> -</ul> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="31" data-paginate="true" data-class="title" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="title" data-marpit-pagination="31" data-marpit-pagination-total="32" style="--paginate:true;--class:title;--theme:default; -;"> -<h1>まとめ</h1> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="32" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Arial", "Hiragino Maru Gothic ProN"; -} - -section.title { - font-size: 40px; - padding: 40px; -} -section.title h1 { - text-align: center; -} - -section.slide h1 { - position: absolute; - left: 50px; top: 35px; -} -" class="slide" data-marpit-pagination="32" data-marpit-pagination-total="32" style="--paginate:true;--class:slide;--theme:default; -;"> -<h1>今後の課題</h1> -<ul> -<li>教育情報システムの周知 -<ul> -<li>Jobの投下やリソースの要求方法</li> -<li>ie-virsh、ie-podmanの使用方法</li> -<li>定期的な周知が必要</li> -</ul> -</li> -<li>ie-podmanのネットワーク構成の見直し -<ul> -<li>プレフィックス長が24のため、最大254個のIPアドレス</li> -<li>コンテナを停止で使用されない場合は削除する必要がある</li> -</ul> -</li> -<li>バックアップの運用 -<ul> -<li>Cephと専用サーバ以外のバックアップ先を用意する必要がある</li> -</ul> -</li> -</ul> -</section> -<script>!function(){"use strict";const t="marpitSVGPolyfill:setZoomFactor,",e=Symbol();let r,o;function n(n){const i="object"==typeof n&&n.target||document,a="object"==typeof n?n.zoom:n;window[e]||(Object.defineProperty(window,e,{configurable:!0,value:!0}),window.addEventListener("message",(({data:e,origin:r})=>{if(r===window.origin)try{if(e&&"string"==typeof e&&e.startsWith(t)){const[,t]=e.split(","),r=Number.parseFloat(t);Number.isNaN(r)||(o=r)}}catch(t){console.error(t)}})));let l=!1;Array.from(i.querySelectorAll("svg[data-marpit-svg]"),(t=>{var e,n,i,s;t.style.transform||(t.style.transform="translateZ(0)");const c=a||o||t.currentScale||1;r!==c&&(r=c,l=c);const d=t.getBoundingClientRect(),{length:u}=t.children;for(let r=0;r<u;r+=1){const o=t.children[r],a=o.getScreenCTM();if(a){const t=null!==(n=null===(e=o.x)||void 0===e?void 0:e.baseVal.value)&&void 0!==n?n:0,r=null!==(s=null===(i=o.y)||void 0===i?void 0:i.baseVal.value)&&void 0!==s?s:0,l=o.firstChild,{style:u}=l;u.transformOrigin||(u.transformOrigin=`${-t}px ${-r}px`),u.transform=`scale(${c}) matrix(${a.a}, ${a.b}, ${a.c}, ${a.d}, ${a.e-d.left}, ${a.f-d.top}) translateZ(0.0001px)`}}})),!1!==l&&Array.from(i.querySelectorAll("iframe"),(({contentWindow:e})=>{null==e||e.postMessage(`${t}${l}`,"null"===window.origin?"*":window.origin)}))}r=1,o=void 0;const i=(t,e,r)=>{if(t.getAttribute(e)!==r)return t.setAttribute(e,r),!0};function a({once:t=!1,target:e=document}={}){const r="Apple Computer, Inc."===navigator.vendor?[n]:[];let o=!t;const a=()=>{for(const t of r)t({target:e});!function(t=document){Array.from(t.querySelectorAll('svg[data-marp-fitting="svg"]'),(t=>{var e;const r=t.firstChild,o=r.firstChild,{scrollWidth:n,scrollHeight:a}=o;let l,s=1;if(t.hasAttribute("data-marp-fitting-code")&&(l=null===(e=t.parentElement)||void 0===e?void 0:e.parentElement),t.hasAttribute("data-marp-fitting-math")&&(l=t.parentElement),l){const t=getComputedStyle(l),e=Math.ceil(l.clientWidth-parseFloat(t.paddingLeft||"0")-parseFloat(t.paddingRight||"0"));e&&(s=e)}const c=Math.max(n,s),d=Math.max(a,1),u=`0 0 ${c} ${d}`;i(r,"width",`${c}`),i(r,"height",`${d}`),i(t,"preserveAspectRatio",getComputedStyle(t).getPropertyValue("--preserve-aspect-ratio")||"xMinYMin meet"),i(t,"viewBox",u)&&t.classList.toggle("__reflow__")}))}(e),o&&window.requestAnimationFrame(a)};return a(),()=>{o=!1}}const l=Symbol(),s=document.currentScript;((t=document)=>{if("undefined"==typeof window)throw new Error("Marp Core's browser script is valid only in browser context.");if(t[l])return t[l];const e=a({target:t}),r=()=>{e(),delete t[l]};Object.defineProperty(t,l,{configurable:!0,value:r})})(s?s.getRootNode():document)}(); -</script></foreignObject></svg></div><script>!function(){"use strict";var e=function(e,t){var n,r=1===(e.parent||e).nodeType?e.parent||e:document.querySelector(e.parent||e),s=[].filter.call("string"==typeof e.slides?r.querySelectorAll(e.slides):e.slides||r.children,(function(e){return"SCRIPT"!==e.nodeName})),a={},i=function(e,t){return(t=t||{}).index=s.indexOf(e),t.slide=e,t},o=function(e,t){a[e]=(a[e]||[]).filter((function(e){return e!==t}))},l=function(e,t){return(a[e]||[]).reduce((function(e,n){return e&&!1!==n(t)}),!0)},c=function(e,t){s[e]&&(n&&l("deactivate",i(n,t)),n=s[e],l("activate",i(n,t)))},d=function(e,t){var r=s.indexOf(n)+e;l(e>0?"next":"prev",i(n,t))&&c(r,t)},u={off:o,on:function(e,t){return(a[e]||(a[e]=[])).push(t),o.bind(null,e,t)},fire:l,slide:function(e,t){if(!arguments.length)return s.indexOf(n);l("slide",i(s[e],t))&&c(e,t)},next:d.bind(null,1),prev:d.bind(null,-1),parent:r,slides:s,destroy:function(e){l("destroy",i(n,e)),a={}}};return(t||[]).forEach((function(e){e(u)})),n||c(0),u};function t(e){e.parent.classList.add("bespoke-marp-parent"),e.slides.forEach((e=>e.classList.add("bespoke-marp-slide"))),e.on("activate",(t=>{const n=t.slide,r=!n.classList.contains("bespoke-marp-active");e.slides.forEach((e=>{e.classList.remove("bespoke-marp-active"),e.setAttribute("aria-hidden","true")})),n.classList.add("bespoke-marp-active"),n.removeAttribute("aria-hidden"),r&&(n.classList.add("bespoke-marp-active-ready"),document.body.clientHeight,n.classList.remove("bespoke-marp-active-ready"))}))}function n(e){let t=0,n=0;Object.defineProperty(e,"fragments",{enumerable:!0,value:e.slides.map((e=>[null,...e.querySelectorAll("[data-marpit-fragment]")]))});const r=r=>void 0!==e.fragments[t][n+r],s=(r,s)=>{t=r,n=s,e.fragments.forEach(((e,t)=>{e.forEach(((e,n)=>{if(null==e)return;const a=t<r||t===r&&n<=s;e.setAttribute("data-bespoke-marp-fragment",a?"active":"inactive"),t===r&&n===s?e.setAttribute("data-bespoke-marp-current-fragment","current"):e.removeAttribute("data-bespoke-marp-current-fragment")}))})),e.fragmentIndex=s;const a={slide:e.slides[r],index:r,fragments:e.fragments[r],fragmentIndex:s};e.fire("fragment",a)};e.on("next",(({fragment:a=!0})=>{if(a){if(r(1))return s(t,n+1),!1;const a=t+1;e.fragments[a]&&s(a,0)}else{const r=e.fragments[t].length;if(n+1<r)return s(t,r-1),!1;const a=e.fragments[t+1];a&&s(t+1,a.length-1)}})),e.on("prev",(({fragment:a=!0})=>{if(r(-1)&&a)return s(t,n-1),!1;const i=t-1;e.fragments[i]&&s(i,e.fragments[i].length-1)})),e.on("slide",(({index:t,fragment:n})=>{let r=0;if(void 0!==n){const s=e.fragments[t];if(s){const{length:e}=s;r=-1===n?e-1:Math.min(Math.max(n,0),e-1)}}s(t,r)})),s(0,0)} +<script>!function(){"use strict";const t="marpitSVGPolyfill:setZoomFactor,",e=Symbol();let r,o;function n(n){const i="object"==typeof n&&n.target||document,a="object"==typeof n?n.zoom:n;window[e]||(Object.defineProperty(window,e,{configurable:!0,value:!0}),window.addEventListener("message",(({data:e,origin:r})=>{if(r===window.origin)try{if(e&&"string"==typeof e&&e.startsWith(t)){const[,t]=e.split(","),r=Number.parseFloat(t);Number.isNaN(r)||(o=r)}}catch(t){console.error(t)}})));let l=!1;Array.from(i.querySelectorAll("svg[data-marpit-svg]"),(t=>{var e,n,i,s;t.style.transform||(t.style.transform="translateZ(0)");const c=a||o||t.currentScale||1;r!==c&&(r=c,l=c);const d=t.getBoundingClientRect(),{length:u}=t.children;for(let r=0;r<u;r+=1){const o=t.children[r],a=o.getScreenCTM();if(a){const t=null!==(n=null===(e=o.x)||void 0===e?void 0:e.baseVal.value)&&void 0!==n?n:0,r=null!==(s=null===(i=o.y)||void 0===i?void 0:i.baseVal.value)&&void 0!==s?s:0,l=o.firstElementChild,{style:u}=l;u.transformOrigin||(u.transformOrigin=`${-t}px ${-r}px`),u.transform=`scale(${c}) matrix(${a.a}, ${a.b}, ${a.c}, ${a.d}, ${a.e-d.left}, ${a.f-d.top}) translateZ(0.0001px)`}}})),!1!==l&&Array.from(i.querySelectorAll("iframe"),(({contentWindow:e})=>{null==e||e.postMessage(`${t}${l}`,"null"===window.origin?"*":window.origin)}))}r=1,o=void 0;const i=(t,e,r)=>{if(t.getAttribute(e)!==r)return t.setAttribute(e,r),!0};function a({once:t=!1,target:e=document}={}){const r="Apple Computer, Inc."===navigator.vendor?[n]:[];let o=!t;const a=()=>{for(const t of r)t({target:e});!function(t=document){Array.from(t.querySelectorAll('svg[data-marp-fitting="svg"]'),(t=>{var e;const r=t.firstChild,o=r.firstChild,{scrollWidth:n,scrollHeight:a}=o;let l,s=1;if(t.hasAttribute("data-marp-fitting-code")&&(l=null===(e=t.parentElement)||void 0===e?void 0:e.parentElement),t.hasAttribute("data-marp-fitting-math")&&(l=t.parentElement),l){const t=getComputedStyle(l),e=Math.ceil(l.clientWidth-parseFloat(t.paddingLeft||"0")-parseFloat(t.paddingRight||"0"));e&&(s=e)}const c=Math.max(n,s),d=Math.max(a,1),u=`0 0 ${c} ${d}`;i(r,"width",`${c}`),i(r,"height",`${d}`),i(t,"preserveAspectRatio",getComputedStyle(t).getPropertyValue("--preserve-aspect-ratio")||"xMinYMin meet"),i(t,"viewBox",u)&&t.classList.toggle("__reflow__")}))}(e),o&&window.requestAnimationFrame(a)};return a(),()=>{o=!1}}const l=Symbol(),s=document.currentScript;((t=document)=>{if("undefined"==typeof window)throw new Error("Marp Core's browser script is valid only in browser context.");if(t[l])return t[l];const e=a({target:t}),r=()=>{e(),delete t[l]};Object.defineProperty(t,l,{configurable:!0,value:r})})(s?s.getRootNode():document)}(); +</script></foreignObject></svg></div><div class="bespoke-marp-note" data-index="1" tabindex="0"><p>研究目的</p></div><div class="bespoke-marp-note" data-index="6" tabindex="0"><p>今までdeleteの話ができる。</p></div><script>!function(){"use strict";var e=function(e,t){var n,r=1===(e.parent||e).nodeType?e.parent||e:document.querySelector(e.parent||e),s=[].filter.call("string"==typeof e.slides?r.querySelectorAll(e.slides):e.slides||r.children,(function(e){return"SCRIPT"!==e.nodeName})),a={},i=function(e,t){return(t=t||{}).index=s.indexOf(e),t.slide=e,t},o=function(e,t){a[e]=(a[e]||[]).filter((function(e){return e!==t}))},l=function(e,t){return(a[e]||[]).reduce((function(e,n){return e&&!1!==n(t)}),!0)},c=function(e,t){s[e]&&(n&&l("deactivate",i(n,t)),n=s[e],l("activate",i(n,t)))},d=function(e,t){var r=s.indexOf(n)+e;l(e>0?"next":"prev",i(n,t))&&c(r,t)},u={off:o,on:function(e,t){return(a[e]||(a[e]=[])).push(t),o.bind(null,e,t)},fire:l,slide:function(e,t){if(!arguments.length)return s.indexOf(n);l("slide",i(s[e],t))&&c(e,t)},next:d.bind(null,1),prev:d.bind(null,-1),parent:r,slides:s,destroy:function(e){l("destroy",i(n,e)),a={}}};return(t||[]).forEach((function(e){e(u)})),n||c(0),u};function t(e){e.parent.classList.add("bespoke-marp-parent"),e.slides.forEach((e=>e.classList.add("bespoke-marp-slide"))),e.on("activate",(t=>{const n=t.slide,r=!n.classList.contains("bespoke-marp-active");e.slides.forEach((e=>{e.classList.remove("bespoke-marp-active"),e.setAttribute("aria-hidden","true")})),n.classList.add("bespoke-marp-active"),n.removeAttribute("aria-hidden"),r&&(n.classList.add("bespoke-marp-active-ready"),document.body.clientHeight,n.classList.remove("bespoke-marp-active-ready"))}))}function n(e){let t=0,n=0;Object.defineProperty(e,"fragments",{enumerable:!0,value:e.slides.map((e=>[null,...e.querySelectorAll("[data-marpit-fragment]")]))});const r=r=>void 0!==e.fragments[t][n+r],s=(r,s)=>{t=r,n=s,e.fragments.forEach(((e,t)=>{e.forEach(((e,n)=>{if(null==e)return;const a=t<r||t===r&&n<=s;e.setAttribute("data-bespoke-marp-fragment",a?"active":"inactive"),t===r&&n===s?e.setAttribute("data-bespoke-marp-current-fragment","current"):e.removeAttribute("data-bespoke-marp-current-fragment")}))})),e.fragmentIndex=s;const a={slide:e.slides[r],index:r,fragments:e.fragments[r],fragmentIndex:s};e.fire("fragment",a)};e.on("next",(({fragment:a=!0})=>{if(a){if(r(1))return s(t,n+1),!1;const a=t+1;e.fragments[a]&&s(a,0)}else{const r=e.fragments[t].length;if(n+1<r)return s(t,r-1),!1;const a=e.fragments[t+1];a&&s(t+1,a.length-1)}})),e.on("prev",(({fragment:a=!0})=>{if(r(-1)&&a)return s(t,n-1),!1;const i=t-1;e.fragments[i]&&s(i,e.fragments[i].length-1)})),e.on("slide",(({index:t,fragment:n})=>{let r=0;if(void 0!==n){const s=e.fragments[t];if(s){const{length:e}=s;r=-1===n?e-1:Math.min(Math.max(n,0),e-1)}}s(t,r)})),s(0,0)} /*! * screenfull -* v5.0.2 - 2020-02-13 +* v5.1.0 - 2020-12-24 * (c) Sindre Sorhus; MIT License */ -var r,s=(function(e){!function(){var t="undefined"!=typeof window&&void 0!==window.document?window.document:{},n=e.exports,r=function(){for(var e,n=[["requestFullscreen","exitFullscreen","fullscreenElement","fullscreenEnabled","fullscreenchange","fullscreenerror"],["webkitRequestFullscreen","webkitExitFullscreen","webkitFullscreenElement","webkitFullscreenEnabled","webkitfullscreenchange","webkitfullscreenerror"],["webkitRequestFullScreen","webkitCancelFullScreen","webkitCurrentFullScreenElement","webkitCancelFullScreen","webkitfullscreenchange","webkitfullscreenerror"],["mozRequestFullScreen","mozCancelFullScreen","mozFullScreenElement","mozFullScreenEnabled","mozfullscreenchange","mozfullscreenerror"],["msRequestFullscreen","msExitFullscreen","msFullscreenElement","msFullscreenEnabled","MSFullscreenChange","MSFullscreenError"]],r=0,s=n.length,a={};r<s;r++)if((e=n[r])&&e[1]in t){for(r=0;r<e.length;r++)a[n[0][r]]=e[r];return a}return!1}(),s={change:r.fullscreenchange,error:r.fullscreenerror},a={request:function(e){return new Promise(function(n,s){var a=function(){this.off("change",a),n()}.bind(this);this.on("change",a);var i=(e=e||t.documentElement)[r.requestFullscreen]();i instanceof Promise&&i.then(a).catch(s)}.bind(this))},exit:function(){return new Promise(function(e,n){if(this.isFullscreen){var s=function(){this.off("change",s),e()}.bind(this);this.on("change",s);var a=t[r.exitFullscreen]();a instanceof Promise&&a.then(s).catch(n)}else e()}.bind(this))},toggle:function(e){return this.isFullscreen?this.exit():this.request(e)},onchange:function(e){this.on("change",e)},onerror:function(e){this.on("error",e)},on:function(e,n){var r=s[e];r&&t.addEventListener(r,n,!1)},off:function(e,n){var r=s[e];r&&t.removeEventListener(r,n,!1)},raw:r};r?(Object.defineProperties(a,{isFullscreen:{get:function(){return Boolean(t[r.fullscreenElement])}},element:{enumerable:!0,get:function(){return t[r.fullscreenElement]}},isEnabled:{enumerable:!0,get:function(){return Boolean(t[r.fullscreenEnabled])}}}),n?e.exports=a:window.screenfull=a):n?e.exports={isEnabled:!1}:window.screenfull={isEnabled:!1}}()}(r={exports:{}},r.exports),r.exports);function a(e){e.fullscreen=()=>{s.isEnabled&&s.toggle(document.body)},document.addEventListener("keydown",(t=>{70!==t.which&&122!==t.which||t.altKey||t.ctrlKey||t.metaKey||!s.isEnabled||(e.fullscreen(),t.preventDefault())}))}function i(e=2e3){return t=>{let n;function r(){n&&clearTimeout(n),n=setTimeout((()=>{t.parent.classList.add("bespoke-marp-inactive"),t.fire("marp-inactive")}),e),t.parent.classList.contains("bespoke-marp-inactive")&&(t.parent.classList.remove("bespoke-marp-inactive"),t.fire("marp-active"))}document.addEventListener("mousedown",r),document.addEventListener("mousemove",r),document.addEventListener("touchend",r),setTimeout(r,0)}}const o=["AUDIO","BUTTON","INPUT","SELECT","TEXTAREA","VIDEO"];function l(e){e.parent.addEventListener("keydown",(e=>{if(!e.target)return;const t=e.target;(o.includes(t.nodeName)||"true"===t.contentEditable)&&e.stopPropagation()}))}function c(e){window.addEventListener("load",(()=>{for(const t of e.slides){const e=t.querySelector("[data-marp-fitting]")?"":"hideable";t.setAttribute("data-bespoke-marp-load",e)}}))}var d;function u({interval:e=200}={}){return t=>{document.addEventListener("keydown",(e=>{if(32===e.which&&e.shiftKey)t.prev();else if(33===e.which||37===e.which||38===e.which)t.prev({fragment:!e.shiftKey});else if(32!==e.which||e.shiftKey)if(34===e.which||39===e.which||40===e.which)t.next({fragment:!e.shiftKey});else if(35===e.which)t.slide(t.slides.length-1,{fragment:-1});else{if(36!==e.which)return;t.slide(0)}else t.next();e.preventDefault()}));let n,r,s=0;t.parent.addEventListener("wheel",(a=>{let i=!1;const o=(e,t)=>{e&&(i=i||function(e,t){return function(e,t){const n=t===d.X?"Width":"Height";return e[`client${n}`]<e[`scroll${n}`]}(e,t)&&function(e,t){const{overflow:n}=e,r=e[`overflow${t}`];return"auto"===n||"scroll"===n||"auto"===r||"scroll"===r}(getComputedStyle(e),t)}(e,t)),(null==e?void 0:e.parentElement)&&o(e.parentElement,t)};if(0!==a.deltaX&&o(a.target,d.X),0!==a.deltaY&&o(a.target,d.Y),i)return;a.preventDefault(),r&&clearTimeout(r),r=setTimeout((()=>{n=0}),e);const l=Date.now()-s<e,c=Math.sqrt(Math.pow(a.deltaX,2)+Math.pow(a.deltaY,2)),u=c<=n;if(n=c,l||u)return;let f;(a.deltaX>0||a.deltaY>0)&&(f="next"),(a.deltaX<0||a.deltaY<0)&&(f="prev"),f&&(t[f](),s=Date.now())}))}}!function(e){e.X="X",e.Y="Y"}(d||(d={}));const f=(...e)=>history.replaceState(...e),m="data-bespoke-view";var p;!function(e){e.Normal="",e.Presenter="presenter",e.Next="next"}(p||(p={}));const h=(e,{protocol:t,host:n,pathname:r,hash:s}=location)=>{const a=e.toString();return`${t}//${n}${r}${a?"?":""}${a}${s}`},g=()=>{switch(document.body.getAttribute(m)){case p.Normal:return p.Normal;case p.Presenter:return p.Presenter;case p.Next:return p.Next;default:throw new Error("View mode is not assigned.")}},v=e=>new URLSearchParams(location.search).get(e),b=(e,t={})=>{const n=Object.assign({location:location,setter:f},t),r=new URLSearchParams(n.location.search);for(const t of Object.keys(e)){const n=e[t];"string"==typeof n?r.set(t,n):r.delete(t)}try{n.setter(null,document.title,h(r,n.location))}catch(e){console.error(e)}},w={available:(()=>{try{return localStorage.setItem("bespoke-marp","bespoke-marp"),localStorage.removeItem("bespoke-marp"),!0}catch(e){return console.warn("Warning: Using localStorage is restricted in the current host so some features may not work."),!1}})(),get:e=>{try{return localStorage.getItem(e)}catch(e){return null}},set:(e,t)=>{try{return localStorage.setItem(e,t),!0}catch(e){return!1}},remove:e=>{try{return localStorage.removeItem(e),!0}catch(e){return!1}}};function y(e=".bespoke-marp-osc"){const t=document.querySelector(e);if(!t)return()=>{};const n=(e,n)=>{t.querySelectorAll(`[data-bespoke-marp-osc=${JSON.stringify(e)}]`).forEach(n)};return s.isEnabled||n("fullscreen",(e=>e.style.display="none")),w.available||n("presenter",(e=>{e.disabled=!0,e.title="Presenter view is disabled due to restricted localStorage."})),e=>{t.addEventListener("click",(t=>{if(t.target instanceof HTMLElement){const{bespokeMarpOsc:n}=t.target.dataset;switch(n&&t.target.blur(),n){case"next":e.next({fragment:!t.shiftKey});break;case"prev":e.prev({fragment:!t.shiftKey});break;case"fullscreen":"function"==typeof e.fullscreen&&s.isEnabled&&e.fullscreen();break;case"presenter":e.openPresenterView()}}})),e.parent.appendChild(t),e.on("activate",(({index:t})=>{n("page",(n=>n.textContent=`Page ${t+1} of ${e.slides.length}`))})),e.on("fragment",(({index:t,fragments:r,fragmentIndex:s})=>{n("prev",(e=>e.disabled=0===t&&0===s)),n("next",(n=>n.disabled=t===e.slides.length-1&&s===r.length-1))})),e.on("marp-active",(()=>t.removeAttribute("aria-hidden"))),e.on("marp-inactive",(()=>t.setAttribute("aria-hidden","true"))),s.isEnabled&&s.onchange((()=>n("fullscreen",(e=>e.classList.toggle("exit",s.isEnabled&&s.isFullscreen)))))}}function x(){const e=Math.max(Math.floor(.85*window.innerWidth),640),t=Math.max(Math.floor(.85*window.innerHeight),360);return window.open(this.presenterUrl,`bespoke-marp-presenter-${this.syncKey}`,`width=${e},height=${t},menubar=no,toolbar=no`)}function k(){const e=new URLSearchParams(location.search);return e.set("view","presenter"),e.set("sync",this.syncKey),h(e)}var E=["area","base","br","col","command","embed","hr","img","input","keygen","link","meta","param","source","track","wbr"];let L=e=>String(e).replace(/[&<>"']/g,(e=>`&${S[e]};`)),S={"&":"amp","<":"lt",">":"gt",'"':"quot","'":"apos"},I="dangerouslySetInnerHTML",P={className:"class",htmlFor:"for"},M={};function N(e,t){let n=[],r="";t=t||{};for(let e=arguments.length;e-- >2;)n.push(arguments[e]);if("function"==typeof e)return t.children=n.reverse(),e(t);if(e){if(r+="<"+e,t)for(let e in t)!1!==t[e]&&null!=t[e]&&e!==I&&(r+=` ${P[e]?P[e]:L(e)}="${L(t[e])}"`);r+=">"}if(-1===E.indexOf(e)){if(t[I])r+=t[I].__html;else for(;n.length;){let e=n.pop();if(e)if(e.pop)for(let t=e.length;t--;)n.push(e[t]);else r+=!0===M[e]?e:L(e)}r+=e?`</${e}>`:""}return M[r]=!0,r}const F=({children:e})=>N(null,null,...e),$="bespoke-marp-presenter-container",O="bespoke-marp-presenter-next",q="bespoke-marp-presenter-next-container",C="bespoke-marp-presenter-note-container",T="bespoke-marp-presenter-info-container",A="bespoke-marp-presenter-info-page",K="bespoke-marp-presenter-info-page-text",j="bespoke-marp-presenter-info-page-prev",R="bespoke-marp-presenter-info-page-next",U="bespoke-marp-presenter-info-time",D="bespoke-marp-presenter-info-timer";function V(e){const{title:t}=document;document.title="[Presenter view]"+(t?` - ${t}`:"");const n={},r=e=>(n[e]=n[e]||document.querySelector(`.${e}`),n[e]);document.body.appendChild((e=>{const t=document.createElement("div");return t.className=$,t.appendChild(e),t.insertAdjacentHTML("beforeend",N(F,null,N("div",{class:q},N("iframe",{class:O,src:"?view=next"})),N("div",{class:C}),N("div",{class:T},N("div",{class:A},N("button",{class:j,tabindex:"-1",title:"Previous"},"Previous"),N("span",{class:K}),N("button",{class:R,tabindex:"-1",title:"Next"},"Next")),N("time",{class:U,title:"Current time"}),N("div",{class:D})))),t})(e.parent)),(e=>{r(q).addEventListener("click",(()=>e.next()));const t=r(O),n=(s=t,(e,t)=>{var n;return null===(n=s.contentWindow)||void 0===n?void 0:n.postMessage(`navigate:${e},${t}`,"null"===window.origin?"*":window.origin)});var s;t.addEventListener("load",(()=>{r(q).classList.add("active"),n(e.slide(),e.fragmentIndex),e.on("fragment",(({index:e,fragmentIndex:t})=>n(e,t)))}));const a=document.querySelectorAll(".bespoke-marp-note");a.forEach((e=>{e.addEventListener("keydown",(e=>e.stopPropagation())),r(C).appendChild(e)})),e.on("activate",(()=>a.forEach((t=>t.classList.toggle("active",t.dataset.index==e.slide()))))),e.on("activate",(({index:t})=>{r(K).textContent=`${t+1} / ${e.slides.length}`}));const i=r(j),o=r(R);i.addEventListener("click",(t=>{i.blur(),e.prev({fragment:!t.shiftKey})})),o.addEventListener("click",(t=>{o.blur(),e.next({fragment:!t.shiftKey})})),e.on("fragment",(({index:t,fragments:n,fragmentIndex:r})=>{i.disabled=0===t&&0===r,o.disabled=t===e.slides.length-1&&r===n.length-1}));const l=()=>r(U).textContent=(new Date).toLocaleTimeString();l(),setInterval(l,250)})(e)}function X(e){const t=g();return t===p.Next&&e.appendChild(document.createElement("span")),e=>{t===p.Normal&&function(e){if(!(e=>e.syncKey&&"string"==typeof e.syncKey)(e))throw new Error("The current instance of Bespoke.js is invalid for Marp bespoke presenter plugin.");Object.defineProperties(e,{openPresenterView:{enumerable:!0,value:x},presenterUrl:{enumerable:!0,get:k}}),w.available&&document.addEventListener("keydown",(t=>{80!==t.which||t.altKey||t.ctrlKey||t.metaKey||(t.preventDefault(),e.openPresenterView())}))}(e),t===p.Presenter&&V(e),t===p.Next&&function(e){const t=t=>{if(t.origin!==window.origin)return;const[n,r]=t.data.split(":");if("navigate"===n){const[t,n]=r.split(",");let s=Number.parseInt(t,10),a=Number.parseInt(n,10)+1;a>=e.fragments[s].length&&(s+=1,a=0),e.slide(s,{fragment:a})}};window.addEventListener("message",t),e.on("destroy",(()=>window.removeEventListener("message",t)))}(e)}}function Y(e){e.on("activate",(t=>{document.querySelectorAll(".bespoke-progress-parent > .bespoke-progress-bar").forEach((n=>{n.style.flexBasis=100*t.index/(e.slides.length-1)+"%"}))}))}const B=e=>{const t=Number.parseInt(e,10);return Number.isNaN(t)?null:t};function z(e={}){const t=Object.assign({history:!0},e);return e=>{let n=!0;const r=e=>{const t=n;try{return n=!0,e()}finally{n=t}},s=(t={fragment:!0})=>{((t,n)=>{const{fragments:r,slides:s}=e,a=Math.max(0,Math.min(t,s.length-1)),i=Math.max(0,Math.min(n||0,r[a].length-1));a===e.slide()&&i===e.fragmentIndex||e.slide(a,{fragment:i})})((B(location.hash.slice(1))||1)-1,t.fragment?B(v("f")||""):null)};e.on("fragment",(({index:e,fragmentIndex:r})=>{n||b({f:0===r||r.toString()},{location:Object.assign(Object.assign({},location),{hash:`#${e+1}`}),setter:(...e)=>t.history?history.pushState(...e):history.replaceState(...e)})})),setTimeout((()=>{s(),window.addEventListener("hashchange",(()=>r((()=>{s({fragment:!1}),b({f:void 0})})))),window.addEventListener("popstate",(()=>{n||r((()=>s()))})),n=!1}),0)}}let H;function W(e={}){const t=e.key||((e=21)=>{let t="",n=crypto.getRandomValues(new Uint8Array(e));for(;e--;){let r=63&n[e];t+=r<36?r.toString(36):r<62?(r-26).toString(36).toUpperCase():r<63?"_":"-"}return t})(),n=`bespoke-marp-sync-${t}`,r=()=>{const e=w.get(n);return e?JSON.parse(e):Object.create(null)},s=e=>{const t=r(),s=Object.assign(Object.assign({},t),e(t));return w.set(n,JSON.stringify(s)),s};return s((e=>({reference:(e.reference||0)+1}))),e=>{Object.defineProperty(e,"syncKey",{value:t,enumerable:!0});let a=!0;setTimeout((()=>{e.on("fragment",(e=>{a&&s((()=>({index:e.index,fragmentIndex:e.fragmentIndex})))}))}),0),window.addEventListener("storage",(t=>{if(t.key===n&&t.oldValue&&t.newValue){const n=JSON.parse(t.oldValue),r=JSON.parse(t.newValue);if(n.index!==r.index||n.fragmentIndex!==r.fragmentIndex)try{a=!1,e.slide(r.index,{fragment:r.fragmentIndex})}finally{a=!0}}})),e.on("destroy",(()=>{const{reference:e}=r();void 0===e||e<=1?w.remove(n):s((()=>({reference:e-1})))}))}}function J({slope:e=Math.tan(-35*Math.PI/180),swipeThreshold:t=30}={}){return n=>{let r;const s=n.parent,a=e=>{const t=s.getBoundingClientRect();return{x:e.pageX-(t.left+t.right)/2,y:e.pageY-(t.top+t.bottom)/2}};s.addEventListener("touchstart",(e=>{r=1===e.touches.length?a(e.touches[0]):void 0}),{passive:!0}),s.addEventListener("touchmove",(e=>{if(r)if(1===e.touches.length){e.preventDefault();const t=a(e.touches[0]),n=t.x-r.x,s=t.y-r.y;r.delta=Math.sqrt(Math.pow(Math.abs(n),2)+Math.pow(Math.abs(s),2)),r.radian=Math.atan2(n,s)}else r=void 0})),s.addEventListener("touchend",(s=>{if(r){if(r.delta&&r.delta>=t&&r.radian){let t=r.radian-e;t=(t+Math.PI)%(2*Math.PI)-Math.PI,n[t<0?"next":"prev"](),s.stopPropagation()}r=void 0}}),{passive:!0})}} +var r,s=(function(e){!function(){var t="undefined"!=typeof window&&void 0!==window.document?window.document:{},n=e.exports,r=function(){for(var e,n=[["requestFullscreen","exitFullscreen","fullscreenElement","fullscreenEnabled","fullscreenchange","fullscreenerror"],["webkitRequestFullscreen","webkitExitFullscreen","webkitFullscreenElement","webkitFullscreenEnabled","webkitfullscreenchange","webkitfullscreenerror"],["webkitRequestFullScreen","webkitCancelFullScreen","webkitCurrentFullScreenElement","webkitCancelFullScreen","webkitfullscreenchange","webkitfullscreenerror"],["mozRequestFullScreen","mozCancelFullScreen","mozFullScreenElement","mozFullScreenEnabled","mozfullscreenchange","mozfullscreenerror"],["msRequestFullscreen","msExitFullscreen","msFullscreenElement","msFullscreenEnabled","MSFullscreenChange","MSFullscreenError"]],r=0,s=n.length,a={};r<s;r++)if((e=n[r])&&e[1]in t){for(r=0;r<e.length;r++)a[n[0][r]]=e[r];return a}return!1}(),s={change:r.fullscreenchange,error:r.fullscreenerror},a={request:function(e,n){return new Promise(function(s,a){var i=function(){this.off("change",i),s()}.bind(this);this.on("change",i);var o=(e=e||t.documentElement)[r.requestFullscreen](n);o instanceof Promise&&o.then(i).catch(a)}.bind(this))},exit:function(){return new Promise(function(e,n){if(this.isFullscreen){var s=function(){this.off("change",s),e()}.bind(this);this.on("change",s);var a=t[r.exitFullscreen]();a instanceof Promise&&a.then(s).catch(n)}else e()}.bind(this))},toggle:function(e,t){return this.isFullscreen?this.exit():this.request(e,t)},onchange:function(e){this.on("change",e)},onerror:function(e){this.on("error",e)},on:function(e,n){var r=s[e];r&&t.addEventListener(r,n,!1)},off:function(e,n){var r=s[e];r&&t.removeEventListener(r,n,!1)},raw:r};r?(Object.defineProperties(a,{isFullscreen:{get:function(){return Boolean(t[r.fullscreenElement])}},element:{enumerable:!0,get:function(){return t[r.fullscreenElement]}},isEnabled:{enumerable:!0,get:function(){return Boolean(t[r.fullscreenEnabled])}}}),n?e.exports=a:window.screenfull=a):n?e.exports={isEnabled:!1}:window.screenfull={isEnabled:!1}}()}(r={exports:{}},r.exports),r.exports);function a(e){e.fullscreen=()=>{s.isEnabled&&s.toggle(document.body)},document.addEventListener("keydown",(t=>{70!==t.which&&122!==t.which||t.altKey||t.ctrlKey||t.metaKey||!s.isEnabled||(e.fullscreen(),t.preventDefault())}))}function i(e=2e3){return t=>{let n;function r(){n&&clearTimeout(n),n=setTimeout((()=>{t.parent.classList.add("bespoke-marp-inactive"),t.fire("marp-inactive")}),e),t.parent.classList.contains("bespoke-marp-inactive")&&(t.parent.classList.remove("bespoke-marp-inactive"),t.fire("marp-active"))}document.addEventListener("mousedown",r),document.addEventListener("mousemove",r),document.addEventListener("touchend",r),setTimeout(r,0)}}const o=["AUDIO","BUTTON","INPUT","SELECT","TEXTAREA","VIDEO"];function l(e){e.parent.addEventListener("keydown",(e=>{if(!e.target)return;const t=e.target;(o.includes(t.nodeName)||"true"===t.contentEditable)&&e.stopPropagation()}))}function c(e){window.addEventListener("load",(()=>{for(const t of e.slides){const e=t.querySelector("[data-marp-fitting]")?"":"hideable";t.setAttribute("data-bespoke-marp-load",e)}}))}var d;function u({interval:e=200}={}){return t=>{document.addEventListener("keydown",(e=>{if(32===e.which&&e.shiftKey)t.prev();else if(33===e.which||37===e.which||38===e.which)t.prev({fragment:!e.shiftKey});else if(32!==e.which||e.shiftKey)if(34===e.which||39===e.which||40===e.which)t.next({fragment:!e.shiftKey});else if(35===e.which)t.slide(t.slides.length-1,{fragment:-1});else{if(36!==e.which)return;t.slide(0)}else t.next();e.preventDefault()}));let n,r,s=0;t.parent.addEventListener("wheel",(a=>{let i=!1;const o=(e,t)=>{e&&(i=i||function(e,t){return function(e,t){const n=t===d.X?"Width":"Height";return e[`client${n}`]<e[`scroll${n}`]}(e,t)&&function(e,t){const{overflow:n}=e,r=e[`overflow${t}`];return"auto"===n||"scroll"===n||"auto"===r||"scroll"===r}(getComputedStyle(e),t)}(e,t)),(null==e?void 0:e.parentElement)&&o(e.parentElement,t)};if(0!==a.deltaX&&o(a.target,d.X),0!==a.deltaY&&o(a.target,d.Y),i)return;a.preventDefault(),r&&clearTimeout(r),r=setTimeout((()=>{n=0}),e);const l=Date.now()-s<e,c=Math.sqrt(Math.pow(a.deltaX,2)+Math.pow(a.deltaY,2)),u=c<=n;if(n=c,l||u)return;let f;(a.deltaX>0||a.deltaY>0)&&(f="next"),(a.deltaX<0||a.deltaY<0)&&(f="prev"),f&&(t[f](),s=Date.now())}))}}!function(e){e.X="X",e.Y="Y"}(d||(d={}));const f=(...e)=>history.replaceState(...e),m="data-bespoke-view";var p;!function(e){e.Normal="",e.Presenter="presenter",e.Next="next"}(p||(p={}));const h=(e,{protocol:t,host:n,pathname:r,hash:s}=location)=>{const a=e.toString();return`${t}//${n}${r}${a?"?":""}${a}${s}`},g=()=>{switch(document.body.getAttribute(m)){case p.Normal:return p.Normal;case p.Presenter:return p.Presenter;case p.Next:return p.Next;default:throw new Error("View mode is not assigned.")}},v=e=>new URLSearchParams(location.search).get(e),b=(e,t={})=>{const n=Object.assign({location:location,setter:f},t),r=new URLSearchParams(n.location.search);for(const t of Object.keys(e)){const n=e[t];"string"==typeof n?r.set(t,n):r.delete(t)}try{n.setter(null,document.title,h(r,n.location))}catch(e){console.error(e)}},w={available:(()=>{try{return localStorage.setItem("bespoke-marp","bespoke-marp"),localStorage.removeItem("bespoke-marp"),!0}catch(e){return console.warn("Warning: Using localStorage is restricted in the current host so some features may not work."),!1}})(),get:e=>{try{return localStorage.getItem(e)}catch(e){return null}},set:(e,t)=>{try{return localStorage.setItem(e,t),!0}catch(e){return!1}},remove:e=>{try{return localStorage.removeItem(e),!0}catch(e){return!1}}};function y(e=".bespoke-marp-osc"){const t=document.querySelector(e);if(!t)return()=>{};const n=(e,n)=>{t.querySelectorAll(`[data-bespoke-marp-osc=${JSON.stringify(e)}]`).forEach(n)};return s.isEnabled||n("fullscreen",(e=>e.style.display="none")),w.available||n("presenter",(e=>{e.disabled=!0,e.title="Presenter view is disabled due to restricted localStorage."})),e=>{t.addEventListener("click",(t=>{if(t.target instanceof HTMLElement){const{bespokeMarpOsc:n}=t.target.dataset;switch(n&&t.target.blur(),n){case"next":e.next({fragment:!t.shiftKey});break;case"prev":e.prev({fragment:!t.shiftKey});break;case"fullscreen":"function"==typeof e.fullscreen&&s.isEnabled&&e.fullscreen();break;case"presenter":e.openPresenterView()}}})),e.parent.appendChild(t),e.on("activate",(({index:t})=>{n("page",(n=>n.textContent=`Page ${t+1} of ${e.slides.length}`))})),e.on("fragment",(({index:t,fragments:r,fragmentIndex:s})=>{n("prev",(e=>e.disabled=0===t&&0===s)),n("next",(n=>n.disabled=t===e.slides.length-1&&s===r.length-1))})),e.on("marp-active",(()=>t.removeAttribute("aria-hidden"))),e.on("marp-inactive",(()=>t.setAttribute("aria-hidden","true"))),s.isEnabled&&s.onchange((()=>n("fullscreen",(e=>e.classList.toggle("exit",s.isEnabled&&s.isFullscreen)))))}}function x(){const e=Math.max(Math.floor(.85*window.innerWidth),640),t=Math.max(Math.floor(.85*window.innerHeight),360);return window.open(this.presenterUrl,`bespoke-marp-presenter-${this.syncKey}`,`width=${e},height=${t},menubar=no,toolbar=no`)}function k(){const e=new URLSearchParams(location.search);return e.set("view","presenter"),e.set("sync",this.syncKey),h(e)}var E=["area","base","br","col","command","embed","hr","img","input","keygen","link","meta","param","source","track","wbr"];let L=e=>String(e).replace(/[&<>"']/g,(e=>`&${S[e]};`)),S={"&":"amp","<":"lt",">":"gt",'"':"quot","'":"apos"},I="dangerouslySetInnerHTML",P={className:"class",htmlFor:"for"},M={};function N(e,t){let n=[],r="";t=t||{};for(let e=arguments.length;e-- >2;)n.push(arguments[e]);if("function"==typeof e)return t.children=n.reverse(),e(t);if(e){if(r+="<"+e,t)for(let e in t)!1!==t[e]&&null!=t[e]&&e!==I&&(r+=` ${P[e]?P[e]:L(e)}="${L(t[e])}"`);r+=">"}if(-1===E.indexOf(e)){if(t[I])r+=t[I].__html;else for(;n.length;){let e=n.pop();if(e)if(e.pop)for(let t=e.length;t--;)n.push(e[t]);else r+=!0===M[e]?e:L(e)}r+=e?`</${e}>`:""}return M[r]=!0,r}const F=({children:e})=>N(null,null,...e),$="bespoke-marp-presenter-container",O="bespoke-marp-presenter-next",q="bespoke-marp-presenter-next-container",C="bespoke-marp-presenter-note-container",T="bespoke-marp-presenter-info-container",A="bespoke-marp-presenter-info-page",K="bespoke-marp-presenter-info-page-text",j="bespoke-marp-presenter-info-page-prev",R="bespoke-marp-presenter-info-page-next",U="bespoke-marp-presenter-info-time",D="bespoke-marp-presenter-info-timer";function V(e){const{title:t}=document;document.title="[Presenter view]"+(t?` - ${t}`:"");const n={},r=e=>(n[e]=n[e]||document.querySelector(`.${e}`),n[e]);document.body.appendChild((e=>{const t=document.createElement("div");return t.className=$,t.appendChild(e),t.insertAdjacentHTML("beforeend",N(F,null,N("div",{class:q},N("iframe",{class:O,src:"?view=next"})),N("div",{class:C}),N("div",{class:T},N("div",{class:A},N("button",{class:j,tabindex:"-1",title:"Previous"},"Previous"),N("span",{class:K}),N("button",{class:R,tabindex:"-1",title:"Next"},"Next")),N("time",{class:U,title:"Current time"}),N("div",{class:D})))),t})(e.parent)),(e=>{r(q).addEventListener("click",(()=>e.next()));const t=r(O),n=(s=t,(e,t)=>{var n;return null===(n=s.contentWindow)||void 0===n?void 0:n.postMessage(`navigate:${e},${t}`,"null"===window.origin?"*":window.origin)});var s;t.addEventListener("load",(()=>{r(q).classList.add("active"),n(e.slide(),e.fragmentIndex),e.on("fragment",(({index:e,fragmentIndex:t})=>n(e,t)))}));const a=document.querySelectorAll(".bespoke-marp-note");a.forEach((e=>{e.addEventListener("keydown",(e=>e.stopPropagation())),r(C).appendChild(e)})),e.on("activate",(()=>a.forEach((t=>t.classList.toggle("active",t.dataset.index==e.slide()))))),e.on("activate",(({index:t})=>{r(K).textContent=`${t+1} / ${e.slides.length}`}));const i=r(j),o=r(R);i.addEventListener("click",(t=>{i.blur(),e.prev({fragment:!t.shiftKey})})),o.addEventListener("click",(t=>{o.blur(),e.next({fragment:!t.shiftKey})})),e.on("fragment",(({index:t,fragments:n,fragmentIndex:r})=>{i.disabled=0===t&&0===r,o.disabled=t===e.slides.length-1&&r===n.length-1}));const l=()=>r(U).textContent=(new Date).toLocaleTimeString();l(),setInterval(l,250)})(e)}function X(e){const t=g();return t===p.Next&&e.appendChild(document.createElement("span")),e=>{t===p.Normal&&function(e){if(!(e=>e.syncKey&&"string"==typeof e.syncKey)(e))throw new Error("The current instance of Bespoke.js is invalid for Marp bespoke presenter plugin.");Object.defineProperties(e,{openPresenterView:{enumerable:!0,value:x},presenterUrl:{enumerable:!0,get:k}}),w.available&&document.addEventListener("keydown",(t=>{80!==t.which||t.altKey||t.ctrlKey||t.metaKey||(t.preventDefault(),e.openPresenterView())}))}(e),t===p.Presenter&&V(e),t===p.Next&&function(e){const t=t=>{if(t.origin!==window.origin)return;const[n,r]=t.data.split(":");if("navigate"===n){const[t,n]=r.split(",");let s=Number.parseInt(t,10),a=Number.parseInt(n,10)+1;a>=e.fragments[s].length&&(s+=1,a=0),e.slide(s,{fragment:a})}};window.addEventListener("message",t),e.on("destroy",(()=>window.removeEventListener("message",t)))}(e)}}function Y(e){e.on("activate",(t=>{document.querySelectorAll(".bespoke-progress-parent > .bespoke-progress-bar").forEach((n=>{n.style.flexBasis=100*t.index/(e.slides.length-1)+"%"}))}))}const B=e=>{const t=Number.parseInt(e,10);return Number.isNaN(t)?null:t};function z(e={}){const t=Object.assign({history:!0},e);return e=>{let n=!0;const r=e=>{const t=n;try{return n=!0,e()}finally{n=t}},s=(t={fragment:!0})=>{((t,n)=>{const{fragments:r,slides:s}=e,a=Math.max(0,Math.min(t,s.length-1)),i=Math.max(0,Math.min(n||0,r[a].length-1));a===e.slide()&&i===e.fragmentIndex||e.slide(a,{fragment:i})})((B(location.hash.slice(1))||1)-1,t.fragment?B(v("f")||""):null)};e.on("fragment",(({index:e,fragmentIndex:r})=>{n||b({f:0===r||r.toString()},{location:Object.assign(Object.assign({},location),{hash:`#${e+1}`}),setter:(...e)=>t.history?history.pushState(...e):history.replaceState(...e)})})),setTimeout((()=>{s(),window.addEventListener("hashchange",(()=>r((()=>{s({fragment:!1}),b({f:void 0})})))),window.addEventListener("popstate",(()=>{n||r((()=>s()))})),n=!1}),0)}}let H;function W(e={}){const t=e.key||((e=21)=>{let t="",n=crypto.getRandomValues(new Uint8Array(e));for(;e--;){let r=63&n[e];t+=r<36?r.toString(36):r<62?(r-26).toString(36).toUpperCase():r<63?"_":"-"}return t})(),n=`bespoke-marp-sync-${t}`,r=()=>{const e=w.get(n);return e?JSON.parse(e):Object.create(null)},s=e=>{const t=r(),s=Object.assign(Object.assign({},t),e(t));return w.set(n,JSON.stringify(s)),s};return s((e=>({reference:(e.reference||0)+1}))),e=>{Object.defineProperty(e,"syncKey",{value:t,enumerable:!0});let a=!0;setTimeout((()=>{e.on("fragment",(e=>{a&&s((()=>({index:e.index,fragmentIndex:e.fragmentIndex})))}))}),0),window.addEventListener("storage",(t=>{if(t.key===n&&t.oldValue&&t.newValue){const n=JSON.parse(t.oldValue),r=JSON.parse(t.newValue);if(n.index!==r.index||n.fragmentIndex!==r.fragmentIndex)try{a=!1,e.slide(r.index,{fragment:r.fragmentIndex})}finally{a=!0}}})),e.on("destroy",(()=>{const{reference:e}=r();void 0===e||e<=1?w.remove(n):s((()=>({reference:e-1})))}))}}function J({slope:e=Math.tan(-35*Math.PI/180),swipeThreshold:t=30}={}){return n=>{let r;const s=n.parent,a=e=>{const t=s.getBoundingClientRect();return{x:e.pageX-(t.left+t.right)/2,y:e.pageY-(t.top+t.bottom)/2}};s.addEventListener("touchstart",(e=>{r=1===e.touches.length?a(e.touches[0]):void 0}),{passive:!0}),s.addEventListener("touchmove",(e=>{if(r)if(1===e.touches.length){e.preventDefault();const t=a(e.touches[0]),n=t.x-r.x,s=t.y-r.y;r.delta=Math.sqrt(Math.pow(Math.abs(n),2)+Math.pow(Math.abs(s),2)),r.radian=Math.atan2(n,s)}else r=void 0})),s.addEventListener("touchend",(s=>{if(r){if(r.delta&&r.delta>=t&&r.radian){let t=r.radian-e;t=(t+Math.PI)%(2*Math.PI)-Math.PI,n[t<0?"next":"prev"](),s.stopPropagation()}r=void 0}}),{passive:!0})}} /*! ***************************************************************************** Copyright (c) Microsoft Corporation.