NL 名古屋で Frege の評価戦略について話してきました

先日の 歌舞伎座.tech に引き続き、NL名古屋 - connpass で Haskell 風 JVM 言語 Frege について発表してきました。

今回の発表では、Frege の持つ Haskell 的特徴である非正格評価に焦点を当て、正格評価を行うはずの Java 上でなぜ評価を遅延させられるのか、その内幕を解説しています。

Frege, What a Non-strict Language from y_taka_23

www.slideshare.net

なお当日の様子は NL名古屋 -NLとはなんだったのか- #nlnagoya - Togetterまとめ にまとめられています。長丁場でしたが、各々さまざまなテーマの発表があり、楽しめるイベントだったと思います。

Java のコード生成を試してみよう！

発表中に述べている通り、Frege のコンパイラはバイトコードではなく Java のソースコードを出力します。ただしスライド中で言及されているコードは Frege が生成した Java コードそのものではなく、今回の内容との関連が薄い部分をわかりやすく改変したものです。ここでは実際にどのようなコンパイル結果が得られるのかを見てみましょう。

コンパイラとコードの準備

Frege の Java 生成ロジックは、最新バージョン v3.24 から大きく変更になりました。今回の発表で述べられているのはこの新しい方のロジックです。

最新のコンパイラはまだ α 版で、各種ビルドツールではまだ使用できないようなので、直接バイナリをダウンロードします。

$ wget -O fregec.jar https://github.com/Frege/frege/releases/download/3.24alpha/frege3.24.61.jar
$ chmod +x fregec.jar

次に、スライド中で登場した竹内のたらい回し関数をサンプルとして使用します。以下の Frege コードを Tarai.fr として保存してください。

module Tarai where

tarai :: Int -> Int -> Int -> Int
tarai x y z =
    if x <= y
        then y
        else tarai (tarai (x - 1) y z)
                   (tarai (y - 1) z x)
                   (tarai (z - 1) x y)

ビルド結果が散らからないように、出力先として build ディレクトリを作成しておきましょう。

$ mkdir build

コンパイル結果の確認

以下のコマンドでコンパイルを実行します。

$ java -Xss1m -jar fregec.jar -d build Tarai.fr

しばらく待つと build 以下に Tarai.java と Tarai.class が生成されます。

今回の目的である build/Tarai.java を確認してみましょう。ファイルの前半はボイラープレートなので無視して、以下の部分が tarai 関数の変換結果です。

final public static int tarai(int arg$1, int arg$2, Lazy<Integer> arg$3) {
  tailrecursion: while (true) {
    final int arg$1f = arg$1;
    final int arg$2f = arg$2;
    final Lazy<Integer> arg$3f = arg$3;
    if (arg$1f <= arg$2f) {
      return arg$2f;
    }
    else {
      arg$1 = Tarai.tarai(arg$1f - 1, arg$2f, arg$3f);
      arg$2 = Tarai.tarai(arg$2f - 1, (int)arg$3f.call(), Thunk.<Integer>lazy(arg$1f));
      arg$3 = Thunk.<Integer>shared(
            (Lazy<Integer>)(() -> Tarai.tarai((int)arg$3f.call() - 1, arg$1f, Thunk.<Integer>lazy(arg$2f)))
          );
      continue tailrecursion;
    }
  }
}

まず気づくこととして、Frege 側の tarai 関数は再帰の形で定義されていましたが、末尾再帰最適化の結果ループ tailrecursion に変換されています。このままだと本題が見えづらいので、Tarai.fr を以下のように書き換えてあえて最適化しないようにしてみましょう。

module Tarai where

tarai :: Int -> Int -> Int -> Int
tarai x y z =
    if x <= y
        then y
        else 0 + tarai (tarai (x - 1) y z)
                       (tarai (y - 1) z x)
                       (tarai (z - 1) x y)

生成される build/Tarai.java は以下のように変化します。

final public static int tarai(final int arg$1, final int arg$2, final Lazy<Integer> arg$3) {
  if (arg$1 <= arg$2) {
    return arg$2;
  }
  else {
    return 0 + Tarai.tarai(
              Tarai.tarai(arg$1 - 1, arg$2, arg$3), Tarai.tarai(arg$2 - 1, (int)arg$3.call(), Thunk.<Integer>lazy(arg$1)),
              Thunk.<Integer>shared(
                    (Lazy<Integer>)(() -> Tarai.tarai((int)arg$3.call() - 1, arg$1, Thunk.<Integer>lazy(arg$2)))
                  )
            );
  }
}

ここから、識別子をわかりやすく x y z に変更して不要な修飾子も削ったものがスライド中に登場したコードです。

static int tarai(int x, int y, Lazy<Integer> z) {
  if (x <= y) {
    return y;
  } else {
    return tarai(
        tarai(x - 1, y, z),
        tarai(y - 1, (int)z.call(), Thunk.<Integer>lazy(x)),
        Thunk.<Integer>shared(
            (Lazy<Integer>)(() -> tarai((int)z.call() - 1, x, Thunk.<Integer>lazy(y))))
    );
  }
}

まとめ

本記事では、発表中に端折り気味だった Java のコード生成部分について、実際のたらい回し関数のコンパイル結果を挙げて補足しました。スライドも合わせて確認してもらえると幸いです。

ちなみに、今回のたらい回し関数は単純に int をとって int を返すだけの関数でした。しかし実際の Frege コードにはもっと複雑な言語機能がいくらでも登場し、

• 高階関数や部分適用のマッピング
• 代数的データ型のマッピング
• モナドのマッピング

などを Java 上で再現するために語るべきことは尽きません。いずれこのブログのネタにでもしますが、それはまた別の話。

歌舞伎座.tech #9 で Frege について話してきました

先日行われた 歌舞伎座.tech#9「異種プログラミング言語格闘勉強会」 - connpass で Haskell 風 JVM 言語である Frege について発表してきました。

今回の勉強会のテーマは「様々な言語に触れて視野を広げる」ということだったので、細かな言語仕様にはあえて触れていません。Frege 自体の紹介と、あとは JVM 言語として一番キャッチーな機能である Java 呼び出しについて解説しました。

すごい Frege たのしく学ぼう！ from y_taka_23

www.slideshare.net

勉強会自体も、マイナ言語の話を一度にこれだけ聞けるというのは珍しくなかなか面白い経験でした。ちなみに個人的に一番の収穫だったのは Pony。歌舞伎座.tech#9でPonyについて発表しました - だいたいよくわからないブログ に発表者のブログ記事があります。

話さなかったこと

今回の発表で触れなかった部分にも、興味を惹くトピックがいくつか残っています。

例えば、今回メインに据えた Java バインディング周りでは

• frege-native-gen について
• 基本型、特に String の扱い
• null や例外の扱い

さらに、Java 呼び出しとは別の Haskell にない機能として

• ドット演算子による Lens 風の関数呼び出し

また、開発環境周りでは

• JVM 系ビルドツールとの連携
• Eclipse Plugin

などが二の矢として温めてある状態です。

これらについては近いうちにこのブログのネタにしようかとも思っているのですが、それはまた別の話。

すごい JVM 言語 Frege をたのしく学ぼう！

言わずと知れた Haskell の定番教科書『すごい Haskell たのしく学ぼう！』に登場するサンプルコードを、プログラミング言語 Frege に翻訳してみました。

github.com

Frege について

Frege は、JVM 上で動く純粋関数型プログラミング言語です。

github.com

最近、JVM 用 Lisp である Clojure の存在感を増してきている気がしますが、Frege はいわばその Haskell 版ですね。

文法的には Haskell + Java のメソッドを呼び出すための追加構文、といった感じ。細かな違いはありますが、Haskell が読める人間であれば理解に苦労することはないでしょう。実際『すごい Haskell』に登場するコードは、大部分が変更なく Frege に「丸写し」することが可能でした。

逆に、Java 方面から入って初めて関数型に挑戦したい人にとってはかなり敷居が高く感じられるはずです。動機として悪くはないと思いますが、良くも悪くも、先に（あるいは同時進行的に）Haskell のさわりを学んでおく必要があるでしょう。

Frege を試すには

Online REPL で実行

環境構築の手間さえ惜しむ怠惰なあなたのために、Web 上で Frege を実行できるデモサイトが用意されています。

• Frege REPL

右ペインにソースコード、左ペインが REPL で、compile ボタンを押すと REPL にモジュールがロードされた状態になります。GHCi と同じノリで使えるのでいろいろ試してみましょう。

コンパイルして実行

前提として JDK 7 もしくは JDK 8 が必要です。JDK 9 は問題が確認されている ので避けましょう。

まず Frege のリリースページ から jar ファイルで提供されているコンパイラをダウンロードします。 この記事を書いている時点での最新バージョンは 3.23.422 です。

$ wget -O fregec.jar https://github.com/Frege/frege/releases/download/3.23.288/frege3.23.422-ga05a487.jar
$ chmod +x fregec.jar

次に、Frege が生成するファイルの書き出し先ディレクトリを準備しておきます。

$ mkdir build

そしてビルドする サンプルコード をダウンロードします。

$ wget https://raw.githubusercontent.com/Frege/frege/release22/examples/SimpleIO.fr

ここまでで、ディレクトリ構造はこんな感じ。

$ tree
.
+--- SimpleIO.fr
+--- build
`--- fregec.jar

以下のコマンドでコンパイルできます。

$ java -Xss1m -jar fregec.jar -d build SimpleIO.fr
$ tree
.
+--- SimpleIO.fr
+--- build
|    `--- examples
|         +--- SimpleIO$1$1.class
|         +--- SimpleIO$1.class
|         +--- SimpleIO$1Fprompt_28850$1.class
|         +--- SimpleIO$1Fprompt_28850.class
|         +--- SimpleIO$2$1.class
|         +--- SimpleIO$2.class
|         +--- SimpleIO$IJ$$mainƒ52393afc.class
|         +--- SimpleIO$IJ$eofƒ5207be3f.class
|         +--- SimpleIO$IJ.class
|         +--- SimpleIO.class
|         `--- SimpleIO.java
`--- fregec.jar

コンパイルされた .class ファイルは以下のコマンドで実行できます。ちなみに SimpleIO の中身は、標準入力から数字を受け取って偶数か奇数かを判定するというものです。

$ java -Xss1m -cp build:fregec.jar examples.SimpleIO

もう少し知りたい人のために

現状、入手できる Frege の情報は残念ながらそれほど多くありません。とりあえず 公式 Wiki を読みましょう。またほぼ全ての関連情報は README 内のリンク集にまとまっています。

文法要素などでわからないところがあるときは、GitHub の Frege リポジトリ内を検索するとヒントが見つかるかもしれません。また、幸か不幸か Frege のコミュニティはとても小さいので、Twitter で #frege タグをつけて英語でツイートすると意外と中の人がアドバイスをくれたりします。

まとめ

今回は、Haskell 風 JVM 言語である Frege について紹介しました。良くも悪くも Haskell に対する理解が必要ではありますが、そこさえ乗り越えてしまえばほぼ Haskell を書きながら Java エコシステムの肩に乗れるという意味でなかなか面白い言語です。

なおこの記事では触れませんでしたが、JVM 言語の例に漏れず Frege から Java のメソッドを呼び出すことが可能で、しかもその方法はかなり巧妙に設計されています。具体的には副作用を持つメソッドを ST モナドにマップするのですが、それはまた別の話。

Alloy で自動定理証明っぽいやつ

このエントリは Theorem Prover Advent Calendar 2015 - Qiita の 23 日目です。

とは言ってみたものの、内容はいわゆる定理証明器の話ではありません。モデル検査器 Alloy を利用して古典命題論理のシークエント計算をモデル化し、証明図を自動生成させることを目標にします。

なお、以下で部分的に引用しているモデル定義の完全版は alloy_sequent.als · GitHub にアップロードしてあります。

モデル化してみる

命題論理式の実装

まず対象となる論理式を Alloy で記述します。

abstract sig Formula {}

sig Atom extends Formula {}

sig Not extends Formula {
    of : one Formula,
}

abstract sig BinaryLogicOperator extends Formula {
    left  : one Formula,
    right : one Formula,
}
sig And, Or, Imply extends BinaryLogicOperator {}

二項演算子たちを定義する際、独立に定義せず間に抽象シグネチャ BinaryLogicOperator を挟んで extends で継承しています。これは Alloy 上の関係には多相性がなく、同じ名前の関係は同じシグネチャ間にしか定義することができないためです。つまり演算子をそれぞれ個別に定義した場合、引数を指す関係名を、例えば andRight : And -> Formula のように演算子ごとにつける必要が生じてしまいます。

そこで、引数を left, right とした BinaryLogicOperator を経由することで、すべての演算子に共通して課したい制約を

fact formulaeAreAcyclic {
    all f : Formula | f not in f.^(of + right + left)
}

のように統一的に記述できるというわけです。

シークエントの実装

さて、次にシークエントの定義を記述します。

sig Sequent {
    antecedents : set Formula,
    succedents  : set Formula,
}

通常の記法で言えばシークエント の が antecedents, が succedents です。

本来、これらは「論理式の列」として個数と順番を考えて保持されるべきですが、今回は古典命題論理しか考えないので個数も順番も無視して単なる集合 set として扱います。部分構造論理が好きな人は潔く諦めましょう。

推論規則の実装

シークエントができたら、推論規則も Alloy に載せましょう。

論理式の場合と同じく、もとになる抽象シグネチャを定義します。

abstract sig InferenceRule {
    premises   : some Sequent,
    conclusion : one Sequent,
}

前提 premises は最大 2 個になり得るので some で、結論 conclusion は必ず 1 個なので one で定義しておきました。

なお、公理は前提が空なる推論規則であると考えて premises を set で定義することも考えられますが、この場合、検証の際に証明図を構成する InferenceRule の数が増えてしまいます。ここでは探索空間の最適化を優先することにして、公理は始シークエント InitialSequent として別途定義することにします。

そして、InferenceRule を継承して個々の推論規則を実装します。今回のように継承先によって異なる性質が要求される場合、Alloy ではシグネチャファクトで制約を記述するのが便利です。例えば以下の規則

sig NotRight extends InferenceRule {
} {
    one premises
    some f : Formula, n : Not {
        f in premises.antecedents
        f in n.of
        n in conclusion.succedents
        premises.antecedents - f = conclusion.antecedents
        premises.succedents = conclusion.succedents - n
    }
}

は否定の導入規則

に対応しています。

同様にして各論理演算子に対応する規則 NotLeft, AndRight, AndLeft, OrRight, OrLeft, ImplyRight, ImplyLeft を定義しておきます。

なお、すでに述べた通りシークエントに登場するコンテクストを集合として実装しているため、構造規則が必要ない（逆に言えば表現できない）ことに留意しましょう。また cut 規則も本質的には必要ないはずなのであらかじめ外しておきます。

証明図の実装

最後に、ここまで登場した要素を積み上げて全体で一つの証明図になるよう制約を加えます。

fact noIsolatedFormulae {
    Formula in Sequent.(antecedents + succedents)
}

sig RootSequent in Sequent {
} {
    this not in InferenceRule.premises
}

sig InitialSequent in Sequent {
} {
    some antecedents & succedents
}

fact rulesFormAProofTree {
    one RootSequent
    Sequent - InferenceRule.conclusion = InitialSequent
    no r : InferenceRule | r in r.^(conclusion.~premises)
    all s : Sequent - InitialSequent | one conclusion.s
}

ここでは、シークエントの中で特殊なポジションを持つものが in 記法により定義されています。 証明されるべき最終的な主張が RootSequent, また公理として扱われる始シーケント

が InitialSequent です (2015/12/23 誤植を修正)。

証明図全体は制約 rulesFormAProofTree により、RouteSequent を根とし、InitialSequent を葉とする二分木になります。

検証してみる

無矛盾性の検証

まず、ここまでに定義した Alloy モデルを使って、矛盾を表す前件、後件ともに空なるシークエントが証明されない（であろう）ことを確認してみましょう。

assert consistency {
    no s : Sequent | s.antecedents = none && s.succedents = none
}
check consistency for 3

assert に対して check を実行すると、Alloy はアサーションに対する反例を探索します。シークエント計算が正しくモデル化されていれば、ここでは反例が発見されないはずです。

排中律の検証

もう一つ、今度は簡単な定理の例として排中律の証明を Alloy に探索させてみましょう。求めるべき主張は なので以下の pred を満たす証明図を run で探索させれば OK です。

pred excludedMiddle {
    some x : Atom, n : Not, o : Or {
        x in o.left
        n in o.right
        x in n.of
        RootSequent.antecedents = none 
        RootSequent.succedents = o
    }
}
run excludedMiddle for 3

以下のような結果が出力されます。

まとめ

とりあえず、今回は試みとして最も単純な古典命題論理のシークエント計算を Alloy でモデル化し、証明を自動探索させてみました。

この他にも例えば、真偽値をシグネチャとして用意し、論理式の評価結果を制約として加えれば、シークエント計算の健全性を示すことができるかもしれません。また、他の体系、例えば直観主義に変更すれば、上で示した排中律の証明は発見できなくなったりするはずです。次なる拡張の方向性はいくつかありそうですが、それはまた別の話。

NGK2015B で AWS + Alloy について話してきました

先日、毎年恒例のなごや LT 大会 NGK2015B / 名古屋合同懇親会 2015 忘年会 で発表してきました。

AWS は形式手法の夢を見るか？ - モデル検査器 Alloy によるインフラ設計 from y_taka_23

www.slideshare.net

当日の動画は [3] NGK2015B（名古屋合同懇親会 2015 忘年会） - YouTube から見ることができます。

TL;DR

• AWS でインフラ運用中
• でも設定が大人の都合でカオスになりがちだったりして辛い
• よろしい、ならば形式手法だ

サンプルコードを動かしてみよう！

まずはインストールしてみる

公式ページ Alloy - download から、jar ファイルで提供されているものをダウンロードしましょう。

java -jar alloy4.2.jar

でウィンドウが起動すれば OK です。

なお、dmg 版も提供されていますが、Mac の人は（少なくとも現状）これをインストールしてはいけません。"Requires Java 6" と宣言している通り、内部のソルバ部分の実装が古い Java ランタイムに依存しているようで、Java 8 では起動できません。ちなみに現在 id:osiire さんが修正版を fork しています。

github.com

早速、検査してみる

今回の LT で使用したサンプルコードが Alloy による AWS セキュリティグループのモデリング · GitHub にあるので、手元にダウンロードして Alloy で開いてみましょう。

そしておもむろに Execute をクリック（または command + E）で

条件に合う設定が自動で探索されるはず。おめでとうございます。これであなたも立派な Alloy エンジニア！

ちょっと条件を変えてみる

Next を押すと、条件に合致する例が次々と表示されるのがわかると思います。しかし数が多すぎるし、各々の違いが解りにくいですね？

探索させる条件である run に対して、それぞれの要素（Alloy では atom と呼びます）の個数を制限することができます。以下のように変更して再度実行してみましょう。

run {
    some disj i1, i2 : Instance, proto : Protocol, port : Port
    | inboundOK[i1, i2, proto, port] &&
      outboundOK[i1, i2, proto, port]
} for 2 Instance, 2 IP, 1 CIDR, 1 SecurityGroup, 2 Rule, 1 Port

ちょっとだけ図がすっきりしました。ちなみに、上記を 1 Rule にすると探索が失敗することも確認してみましょう。インスタンス間の通信が成立するためにはインバウンドルールとアウトバウンドルールが少なくとも 1 つずつ必要ですからね。

さて、セキュリティグループのルールに直接 CIDR を指定すると、何のサーバなのかわからないし、後々管理が辛くなりそうですね？「すべてのルールについて、source / destination は（CIDR ではなく）セキュリティグループ名で指定する」という制約を加えるには以下のようにすれば OK。

run {
    some disj i1, i2 : Instance, proto : Protocol, port : Port
    | inboundOK[i1, i2, proto, port] &&
      outboundOK[i1, i2, proto, port]
    Rule.(source + destination) in SecurityGroup
}

他にも思いつく制約をいろいろ試してみましょう。

そしてその先へ……

さて、Alloy を少し触ってみてちょっと面白そうだと思ったあなたに、第一にお勧めしたいのがこちら。

www.amazon.co.jp

Alloy の背景にある関係モデルも含めてしっかり解説されており、密度の高い良書です。サンプルや練習問題も trivial なものから歯ごたえのあるものまで幅広く掲載されており、これを完全にフォローすれば Alloy を使う上でもはや不足はないと言ってよいでしょう。

また、書名に Alloy は入っていないのですが、こちらの書籍も面白いと思います。

www.amazon.co.jp

Alloy そのものというよりは、実際の仕様や開発ライフサイクルに対してどのように形式手法が関わるのかについて焦点を当てた、より実務者向けの参考書です。

ところで自分はといえば、

例の Alloy 本はとてもよい教科書だと思うのだけれど、如何せん敷居が高い。いつかあのエッセンスを抽出したもっとフレンドリなチュートリアルを書きたい。

— チェシャ猫 (@y_taka_23) 2015, 10月 5

みたいな野望があったりなかったりするのですが、それはまた別の話。

第十二回渋谷 Java で Featherweight Java の話をしてきました

8 月 1 日に行われた第十二回渋谷 Java で Java の型システムについて LT をしてきました。以下が使用したスライドです。

Hello, Type Systems! - Introduction to Featherweight Java from y_taka_23

ちなみに Featherweight Java を導入した論文はここで読めます。今回の LT では時間の都合上細かい内容をほとんど述べていないので、もし興味があればぜひ元論文に目を通してみると面白いと思います。なお LT で扱ったのは第 2 章で述べられている（ジェネリクスを持たない）FJ の部分です。

スライドの補足

型付け規則と簡約規則について、時間の制限もあり LT の中では例を 1 つずつ挙げるだけに留めました。しかしそのせいでスライド 25 ページ目の主張で "two impolite rules" という表現を用いて規則の詳細から逃げています。

元論文の系 2.4.6 (p.408) を見て頂ければおわかりのように、ここで言っている "two impolite rules" は

• ダウンキャスト式の型付け (p.404, Fig. 2, T-DCast)
• ダウンでもアップでもないキャスト式の型付け (p.404, Fig. 2, T-SCast)

のことを指しています。FJ において、この 2 つの規則を用いずに型が付く式については正規系まで簡約したときに結果が値である、というのがもともとの主張です。

ジェネリクスの意味論

今回はシンプルな FJ についてのみ触れましたが、元論文ではこの後にジェネリクスを導入した体系 Featherweight GJ が論じられています。というより、分量的にもジェネリクスの方が元論文の「本体」で、今回紹介できた部分はいわばその前哨戦。

もし何か機会があればこのジェネリクスについても話したいと思っているのですが、それはまた別の話。

稼働中の Docker コンテナ内にファイルを転送するツール Docker Inject を作ってみました

ホスト側から run 中の Docker コンテナ内へ、ディレクトリごとコピーします。

github.com

背景

Docker を運用している上で、動いているコンテナの中にファイルを送り込みたくなったことはないでしょうか。ないですか？ 残念ながらあるところにはあるのです。とりあえず今回はあるということにして進みます。

docker cp コマンドを使用すれば「コンテナからホストへ」のファイル転送は可能ですが、逆に「ホストからコンテナへ」の転送手段は公式では提供されていないはずです。docker run 時に -v オプションを付けておいて、マウントされたディレクトリをファイルの受け渡し場所として使用することも不可能ではないですが、ご存知の通りすでに稼働しているコンテナに後から -v を設定することはできません。

無論、コンテナにファイルを送り込むと Dockerfile とコンテナの状態とが乖離することになるため、いわゆる immutable infrastructure の観点からは邪道です。公式で提供されていない理由もそのあたりにあるのでしょう。理想を言えばそういう状況は発生しないに越したことはないのですが、現実というやつはいとも簡単に我々を裏切るわけで、まあそういう経緯でこのツールは制作されました。

インストール

今回は Go のクロスコンパイル機能を使ってバイナリ配布にしてみました。解凍して出てきた実行ファイルを PATH が通っている場所に置けばそのまま使えます。

Releases · y-taka-23/docker-inject · GitHub

あるいは Go の処理系が手元にあるなら go get でも使用可能になります。

$ go get https://github.com/y-taka-23/docker-inject

使い方

docker-inject <コピー元> <コンテナ名>:<コピー先> で動作します。

ちなみに Windows の場合、<コピー元> のパスは \ 区切りですが、<コピー先> は Linux なので / 区切りで指定する必要があるのでご注意を。

動作原理

基本的には以下のようなコマンドを実行しているだけです。

$ docker exec -i <コンテナ名> bash -c 'cat > <コピー先ファイル>' < <コピー元ファイル>

これを実行すると

• docker exec でコンテナ内でコマンドを実行
• その際 -i オプションによりホスト側の標準入力がコンテナ内の標準入力に接続される
• ホスト側ではコピー元ファイルを標準入力に流し込む
• コンテナ内では cat が標準入力の内容をコピー先ファイルに書き出す

という過程を経て、ホスト側のファイルがコンテナ内に書き出されます。

直したいところ

現状の問題点として、以下がすぐに思いつきます。

• ファイルごとに毎回 docker exec を実行しているため動作が遅い
• コピー先のファイルは上書きされる。-f とか -u オプションがない。

可能ならばいずれこの辺も対応したいところではありますが、それはまた別の話。