deploy: 8785c14

hello-world/cat.html

@@ -176,7 +176,7 @@ <h2 id="getting-started"><a class="header" href="#getting-started">Getting start
   IO.println s!&quot;Hello, cats!&quot;
 </code></pre>
 <p>Alternatively, running <code>lake new feline exe</code> instructs <code>lake</code> to use a template that does not include a library section, making it unnecessary to edit the file.</p>
-<p>Ensure that the code can be built by running <code>{{#command {feline/1} {feline/1} {lake build} }}</code>.</p>
+<p>Ensure that the code can be built by running <code>lake build</code>.</p>
 <h2 id="concatenating-streams"><a class="header" href="#concatenating-streams">Concatenating Streams</a></h2>
 <p>Now that the basic skeleton of the program has been built, it's time to actually enter the code.
 A proper implementation of <code>cat</code> can be used with infinite IO streams, such as <code>/dev/random</code>, which means that it can't read its input into memory before outputting it.
@@ -293,12 +293,12 @@ <h3 id="main"><a class="header" href="#main">Main</a></h3>
   | _ =&gt;  process 0 args
 </code></pre>
 <h2 id="meow"><a class="header" href="#meow">Meow!</a></h2>
-<p>To check whether <code>feline</code> works, the first step is to build it with <code>{{#command {feline/2} {feline/2} {lake build} }}</code>.
+<p>To check whether <code>feline</code> works, the first step is to build it with <code>lake build</code>.
 First off, when called without arguments, it should emit what it receives from standard input.
 Check that</p>
-<pre><code>{{#command {feline/2} {feline/2} {echo &quot;It works!&quot; | ./build/bin/feline} }}
+<pre><code>echo &quot;It works!&quot; | ./build/bin/feline
 </code></pre>
-<p>emits <code>{{#command_out {feline/2} {echo &quot;It works!&quot; | ./build/bin/feline} }}</code>.</p>
+<p>emits <code>It works!</code>.</p>
 <p>Secondly, when called with files as arguments, it should print them.
 If the file <code>test1.txt</code> contains</p>
 <pre><code>It's time to find a warm spot
@@ -307,16 +307,19 @@ <h2 id="meow"><a class="header" href="#meow">Meow!</a></h2>
 <pre><code>and curl up!
 </code></pre>
 <p>then the command</p>
-<pre><code>{{#command {feline/2} {feline/2} {./build/bin/feline test1.txt test2.txt} }}
+<pre><code>./build/bin/feline test1.txt test2.txt
 </code></pre>
 <p>should emit</p>
-<pre><code>{{#command_out {feline/2} {./build/bin/feline test1.txt test2.txt} {feline/2/expected/test12.txt} }}
+<pre><code>It's time to find a warm spot
+and curl up!
 </code></pre>
 <p>Finally, the <code>-</code> argument should be handled appropriately.</p>
-<pre><code>{{#command {feline/2} {feline/2} {echo &quot;and purr&quot; | ./build/bin/feline test1.txt - test2.txt} }}
+<pre><code>echo &quot;and purr&quot; | ./build/bin/feline test1.txt - test2.txt
 </code></pre>
 <p>should yield</p>
-<pre><code>{{#command_out {feline/2} {echo &quot;and purr&quot; | ./build/bin/feline test1.txt - test2.txt} {feline/2/expected/test1purr2.txt}}}
+<pre><code>It's time to find a warm spot
+and purr
+and curl up!
 </code></pre>
 <h2 id="exercise"><a class="header" href="#exercise">Exercise</a></h2>
 <p>Extend <code>feline</code> with support for usage information.

hello-world/running-a-program.html

@@ -154,12 +154,12 @@ <h1 id="プログラムの実行"><a class="header" href="#プログラムの実
 Then, from the command line, run:
 -->
 <p>次に，コマンドラインから以下を実行してください．</p>
-<pre><code>{{#command {simple-hello} {hello} {lean --run Hello.lean} }}
+<pre><code>lean --run Hello.lean
 </code></pre>
 <!--
-The program displays `{{#command_out {hello} {lean --run Hello.lean} }}` and exits.
+The program displays `Hello, world!` and exits.
 -->
-<p>このプログラムは <code>{{#command_out {hello} {lean --run Hello.lean} }}</code> を表示して終了します．</p>
+<p>このプログラムは <code>Hello, world!</code> を表示して終了します．</p>
 <!-- ## Anatomy of a Greeting -->
 <h2 id="挨拶の構造"><a class="header" href="#挨拶の構造">挨拶の構造</a></h2>
 <!--
@@ -287,13 +287,15 @@ <h2 id="ioアクションの結合"><a class="header" href="#ioアクション
 This program can be run in the same manner as the prior program:
 -->
 <p>このプログラムは，前のプログラムと同じ方法で実行できます．</p>
-<pre><code>{{#command {hello-name} {hello-name} {./run} {lean --run HelloName.lean}}}
+<pre><code>lean --run HelloName.lean
 </code></pre>
 <!--
 If the user responds with `David`, a session of interaction with the program reads:
 -->
 <p>ユーザが<code>David</code>と応答する場合，プログラムとの対話セッションが次のように表示されます．</p>
-<pre><code>{{#command_out {hello-name} {./run} }}
+<pre><code>How would you like to be addressed?
+David
+Hello, David!
 </code></pre>
 <!--
 The type signature line is just like the one for `Hello.lean`:

hello-world/starting-a-project.html

@@ -151,7 +151,7 @@ <h1 id="starting-a-project"><a class="header" href="#starting-a-project">Startin
 They are <em>embedded</em> because they occur inside another language's syntax.
 While Lean contains rich facilities for creating EDSLs, they are beyond the scope of this book.</p>
 <h2 id="first-steps"><a class="header" href="#first-steps">First steps</a></h2>
-<p>To get started with a project that uses Lake, use the command <code>{{#command {first-lake} {lake} {lake new greeting} }}</code> in a directory that does not already contain a file or directory called <code>greeting</code>.
+<p>To get started with a project that uses Lake, use the command <code>lake new greeting</code> in a directory that does not already contain a file or directory called <code>greeting</code>.
 This creates a directory called <code>greeting</code> that contains the following files:</p>
 <ul>
 <li><code>Main.lean</code> is the file in which the Lean compiler will look for the <code>main</code> action.</li>
@@ -163,28 +163,48 @@ <h2 id="first-steps"><a class="header" href="#first-steps">First steps</a></h2>
 Typically, the majority of the application logic will be in a collection of libraries for the program, while <code>Main.lean</code> will contain a small wrapper around these pieces that does things like parsing command lines and executing the central application logic.
 To create a project in an already-existing directory, run <code>lake init</code> instead of <code>lake new</code>.</p>
 <p>By default, the library file <code>Greeting/Basic.lean</code> contains a single definition:</p>
-<pre><code class="language-lean">{{#file_contents {lake} {first-lake/greeting/Greeting/Basic.lean} {first-lake/expected/Greeting/Basic.lean}}}
+<pre><code class="language-lean">def hello := &quot;world&quot;
 </code></pre>
 <p>The library file <code>Greeting.lean</code> imports <code>Greeting/Basic.lean</code>:</p>
-<pre><code class="language-lean">{{#file_contents {lake} {first-lake/greeting/Greeting.lean} {first-lake/expected/Greeting.lean}}}
+<pre><code class="language-lean">-- This module serves as the root of the `Greeting` library.
+-- Import modules here that should be built as part of the library.
+import «Greeting».Basic
 </code></pre>
 <p>This means that everything defined in <code>Greetings/Basic.lean</code> is also available to files that import <code>Greetings.lean</code>.
 In <code>import</code> statements, dots are interpreted as directories on disk.
 Placing guillemets around a name, as in <code>«Greeting»</code>, allow it to contain spaces or other characters that are normally not allowed in Lean names, and it allows reserved keywords such as <code>if</code> or <code>def</code> to be used as ordinary names by writing <code>«if»</code> or <code>«def»</code>.
 This prevents issues when the package name provided to <code>lake new</code> contains such characters.</p>
 <p>The executable source <code>Main.lean</code> contains:</p>
-<pre><code class="language-lean">{{#file_contents {lake} {first-lake/greeting/Main.lean} {first-lake/expected/Main.lean}}}
+<pre><code class="language-lean">import «Greeting»
+
+def main : IO Unit :=
+  IO.println s!&quot;Hello, {hello}!&quot;
 </code></pre>
 <p>Because <code>Main.lean</code> imports <code>Greetings.lean</code> and <code>Greetings.lean</code> imports <code>Greetings/Basic.lean</code>, the definition of <code>hello</code> is available in <code>main</code>.</p>
-<p>To build the package, run the command <code>{{#command {first-lake/greeting} {lake} {lake build} }}</code>.
+<p>To build the package, run the command <code>lake build</code>.
 After a number of build commands scroll by, the resulting binary has been placed in <code>build/bin</code>.
-Running <code>{{#command {first-lake/greeting} {lake} {./build/bin/greeting} }}</code> results in <code>{{#command_out {lake} {./build/bin/greeting} }}</code>.</p>
+Running <code>./build/bin/greeting</code> results in <code>Hello, world!</code>.</p>
 <h2 id="lakefiles"><a class="header" href="#lakefiles">Lakefiles</a></h2>
 <p>A <code>lakefile.lean</code> describes a <em>package</em>, which is a coherent collection of Lean code for distribution, analogous to an <code>npm</code> or <code>nuget</code> package or a Rust crate.
 A package may contain any number of libraries or executables.
 While the <a href="https://github.com/leanprover/lake#readme">documentation for Lake</a> describes the available options in a lakefile, it makes use of a number of Lean features that have not yet been described here.
 The generated <code>lakefile.lean</code> contains the following:</p>
-<pre><code class="language-lean">{{#file_contents {lake} {first-lake/greeting/lakefile.lean} {first-lake/expected/lakefile.lean}}}
+<pre><code class="language-lean">import Lake
+open Lake DSL
+
+package «greeting» where
+  -- add package configuration options here
+
+lean_lib «Greeting» where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe «greeting» where
+  root := `Main
+  -- Enables the use of the Lean interpreter by the executable (e.g.,
+  -- `runFrontend`) at the expense of increased binary size on Linux.
+  -- Remove this line if you do not need such functionality.
+  supportInterpreter := true
 </code></pre>
 <p>This initial Lakefile consists of three items:</p>
 <ul>
@@ -211,10 +231,14 @@ <h2 id="libraries-and-imports"><a class="header" href="#libraries-and-imports">L
 <p>Additional module files may be added to the library by creating a directory called <code>Greeting</code> and placing them inside.
 These names can be imported by replacing the directory separator with a dot.
 For instance, creating the file <code>Greeting/Smile.lean</code> with the contents:</p>
-<pre><code class="language-lean">{{#file_contents {lake} {second-lake/greeting/Greeting/Smile.lean}}}
+<pre><code class="language-lean">def expression : String := &quot;a big smile&quot;
 </code></pre>
 <p>means that <code>Main.lean</code> can use the definition as follows:</p>
-<pre><code class="language-lean">{{#file_contents {lake} {second-lake/greeting/Main.lean}}}
+<pre><code class="language-lean">import Greeting
+import Greeting.Smile
+
+def main : IO Unit :=
+  IO.println s!&quot;Hello, {hello}, with {expression}!&quot;
 </code></pre>
 <p>The module name hierarchy is decoupled from the namespace hierarchy.
 In Lean, modules are units of code distribution, while namespaces are units of code organization.