diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml index 0ca68b36..5fc8ea56 100644 --- a/.github/workflows/blueprint.yml +++ b/.github/workflows/blueprint.yml @@ -23,6 +23,10 @@ permissions: pull-requests: write # Write access to pull requests actions: write # Write access to GitHub Actions +env: + LEAN_EXPOSITION_REPO: LeanMachineLearning/exposition + LEAN_EXPOSITION_REF: main + jobs: build_project: runs-on: ubuntu-latest @@ -55,6 +59,26 @@ jobs: run: | ./scripts/build_docs.sh + - name: Clone lean-exposition + run: | + git clone --depth 1 --branch "$LEAN_EXPOSITION_REF" \ + "https://github.com/$LEAN_EXPOSITION_REPO" /tmp/lean-exposition + + - name: Build exposition binary + run: | + cd /tmp/lean-exposition && lake build exposition + echo "EXPOSITION_BIN=/tmp/lean-exposition/.lake/build/bin/exposition" >> "$GITHUB_ENV" + + - name: Build exposition documentation + run: | + lake env "$EXPOSITION_BIN" \ + --root LeanMachineLearning \ + --repo-url https://github.com/LeanMachineLearning/LML \ + --output ./exposition \ + --exclude-lib LMLTutorial + mkdir -p home_page/exposition + cp -r exposition/html-multi/* home_page/exposition + - name: Compile blueprint and documentation uses: leanprover-community/docgen-action@7b5b9a1822650bd45aaeb4182d94bceba2030f89 # 2026-04-14 with: diff --git a/.gitignore b/.gitignore index 8b05af42..acf454ad 100644 --- a/.gitignore +++ b/.gitignore @@ -40,6 +40,7 @@ blueprint/src/web.pdf ## Website /home_page/ +/exposition/ ## Tutorial and docs /LMLTutorial/.lake/ diff --git a/LMLDocs.lean b/LMLDocs.lean deleted file mode 100644 index aab0bd6a..00000000 --- a/LMLDocs.lean +++ /dev/null @@ -1,4 +0,0 @@ -import LMLDocs.Docs -import LMLDocs.Front -import LMLDocs.Pages.BasicProbability -import LMLDocs.References diff --git a/LMLDocs/Docs.lean b/LMLDocs/Docs.lean deleted file mode 100644 index d16d7601..00000000 --- a/LMLDocs/Docs.lean +++ /dev/null @@ -1,19 +0,0 @@ -import VersoManual - -import LMLDocs.Front - -open Verso.Genre.Manual Verso.Output.Html - -def extraHead : Array Verso.Output.Html := #[ - {{}}, - {{}}, - {{}}, -] - -def config : RenderConfig := { - extraHead := extraHead, - sourceLink := some "https://github.com/LeanMachineLearning/LML", - issueLink := some "https://github.com/LeanMachineLearning/LML/issues", -} - -def main := manualMain (%doc LMLDocs.Front) (config := config) diff --git a/LMLDocs/Front.lean b/LMLDocs/Front.lean deleted file mode 100644 index 8c30526c..00000000 --- a/LMLDocs/Front.lean +++ /dev/null @@ -1,23 +0,0 @@ -import LMLDocs.Pages.BasicProbability -import VersoManual - -set_option linter.style.header false -set_option linter.style.setOption false -set_option linter.hashCommand false -set_option linter.style.longLine false -set_option pp.rawOnError true -set_option verso.code.warnLineLength 100 - -open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External - -#doc (Manual) "Lean Machine Learning" => -%%% -authors := [] -shortTitle := "Lean Machine Learning" -%%% - -These documentation pages are a manual prototype for definition certification pages for the [Lean Machine Learning](https://leanmachinelearning.org) library. - -Some of it should be automatically generated from the code, but for now it is mostly written by hand. - -{include 0 LMLDocs.Pages.BasicProbability} diff --git a/LMLDocs/Pages/BasicProbability.lean b/LMLDocs/Pages/BasicProbability.lean deleted file mode 100644 index 3940b022..00000000 --- a/LMLDocs/Pages/BasicProbability.lean +++ /dev/null @@ -1,130 +0,0 @@ -/- -Copyright (c) 2025 Rémy Degenne. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne --/ -import VersoManual -import Mathlib.Probability.Distributions.Gaussian.Real -import Mathlib.Probability.Independence.Basic -import Mathlib.Probability.Moments.Basic - -set_option linter.style.header false -set_option linter.style.setOption false -set_option linter.hashCommand false -set_option linter.style.longLine false -set_option pp.rawOnError true -set_option verso.code.warnLineLength 100 - -open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External - -#doc (Manual) "Probability Spaces and Measures" => -%%% -htmlSplit := .never -%%% - -```lean -show -open MeasureTheory ProbabilityTheory -open scoped ENNReal NNReal -``` - -First, in order to work on probability we need a measurable space. -We can define a probability measure on such a space as follows. -```lean -variable {Ω : Type*} [MeasurableSpace Ω] - {P : Measure Ω} [IsProbabilityMeasure P] -``` -The class `MeasurableSpace Ω` defines a sigma-algebra on `Ω`. We then introduced a measure `P` on that sigma-algebra and specified that it should be a probability measure. -If we want to work on `ℝ` or another well known type the typeclass inference system will find `[MeasurableSpace ℝ]` on its own. We can write simply -```lean -variable {P : Measure ℝ} [IsProbabilityMeasure P] -``` - -With the code above, we can introduce several probability measures on the same space. When using lemmas and definitions about those measures, we will need to specify which measure we are talking about. -For example, the variance of a random variable `X` with respect to the measure `P` will be `variance X P`. - -But perhaps we just want a space with a canonical probability measure, which would be the one used without us having to tell Lean explicitly. -That can be done with the `MeasureSpace` class. A `MeasureSpace` is a `MeasurableSpace` with a canonical measure called `volume`. -The probability library of Mathlib defines a notation `ℙ` for that measure. We still need to tell that we want it to be a probability measure though. -```lean -variable {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)] -``` -Remark 1: in the code above we can't write only `[IsProbabilityMeasure ℙ]` because Lean would then not know to which space the default measure `ℙ` refers to. -That will not be necessary when we use `ℙ` in proofs because the context will be enough to infer `Ω`. - -Remark 2: a lemma written for `P : Measure Ω` in a `MeasurableSpace Ω` will apply for the special measure `ℙ` in a `MeasureSpace Ω`, but the converse is not true. -Mathlib focuses on generality, hence uses the `MeasurableSpace` spelling for its lemmas. In another context, the convenience of `MeasureSpace` may be preferable. - - -Remark 3: `IsProbabilityMeasure` vs `ProbabilityMeasure`. -The examples above used `{P : Measure Ω} [IsProbabilityMeasure P]` to define a probability measure. That's the standard way to do it. -Mathlib also contains a type `ProbabilityMeasure Ω`: the subtype of measures that are probability measures. -The goal of that type is to work on the set of probability measures on `Ω`. -In particular, it comes with a topology, the topology of convergence in distribution (weak convergence of measures). -If we don't need to work with that topology, `{P : Measure Ω} [IsProbabilityMeasure P]` should be preferred. - - -# Probability of events - -An event is a measurable set: there is no special event definition in Mathlib. -The probability of that event is the measure of the set. -A `Measure` can be applied to a set like a function and returns a value in `ENNReal` (denoted by `ℝ≥0∞`, available after `open scoped ENNReal`). -```lean -example (P : Measure ℝ) (s : Set ℝ) : ℝ≥0∞ := P s -``` -The probability of the event `s` is thus `P s`. -The type `ℝ≥0∞` represents the nonnegative reals and infinity: the measure of a set is a nonnegative real number which in general may be infinite. -If `P` is a probability measure, it actually takes only values up to 1. -The tactic `simp` knows that a probability measure is finite and will use the lemmas `measure_ne_top` or `measure_lt_top` to prove that `P s ≠ ∞` or `P s < ∞`. - -The operations on `ℝ≥0∞` are not as nicely behaved as on `ℝ`: `ℝ≥0∞` is not a ring. For example, subtraction truncates to zero. -If one finds that lemma `lemma_name` used to transform an equation does not apply to `ℝ≥0∞`, a good thing to try is to find a lemma named like `ENNReal.lemma_name_of_something` and use that instead (it will typically require that one variable is not infinite). - -For many lemmas to apply, the set `s` will need to be a measurable set. The way to express that is `MeasurableSet s`. - - -# Random variables - -A random variable is a measurable function from a measurable space to another. -```lean -variable {Ω : Type*} [MeasurableSpace Ω] {X : Ω → ℝ} (hX : Measurable X) -``` -In that code we defined a random variable `X` from the measurable space `Ω` to `ℝ` (for which the typeclass inference system finds a measurable space instance). The assumption `hX` states that `X` is measurable, which is necessary for most manipulations. - -If we define a measure `P` on `Ω`, we can talk about the law or distribution of a random variable `X : Ω → E`. -The law of `X` is a measure on `E`, with value `P (X ⁻¹' s)` on any measurable set `s` of `E`. -This is how we define the map of the measure `P` by `X`, `Measure.map X P` or more succinctly `P.map X`. -There is no specific notation for that law. -To say that `X` is Gaussian with mean 0 and variance 1, write `P.map X = gaussianReal 0 1`. - -The expectation of `X` is the integral of that function against the measure `P`, written `∫ ω, X ω ∂P`. -The notation `P[X]` is shorthand for that expectation. In a `MeasureSpace`, we can further use the notation `𝔼[X]`. - -Remark: there are two types of integrals in Mathlib, Bochner integrals and Lebesgue integrals. -The expectation notations stand for the Bochner integral, which is defined for `X : Ω → E` with `E` a normed space over `ℝ` (`[NormedAddCommGroup E] [NormedSpace ℝ E]`). -They don't work for `Y : Ω → ℝ≥0∞` since `ℝ≥0∞` is not a normed space, but those functions can be integrated with the Lebesgue integral: `∫⁻ ω, Y ω ∂P`. -There is no expectation notation for the Lebesgue integral. - -# Discrete probability - -In discrete probability, measurability is not an issue: every set and every function are measurable. -The typeclass `[DiscreteMeasurableSpace Ω]` signals that every set of `Ω` is measurable and the lemma `MeasurableSet.of_discrete` provides a proof of measurability. -To obtain measurability of a function from `Ω`, use `Measurable.of_discrete`. - -Any countable type with measurable singletons is a `DiscreteMeasurableSpace`, for example `ℕ` or `Fin n`. - -A way to define a probability measure on a discrete space `Ω` is to use the type `PMF Ω`, which stands for probability mass function. -`PMF Ω` is the subtype of functions `Ω → ℝ≥0∞` that sum to 1. -One can get a `Measure Ω` from `p : PMF Ω` with `p.toMeasure`. -When writing a theorem about probability on finite spaces, it preferable to write it for a `Measure` in a `DiscreteMeasurableSpace` than for a `PMF` for better integration with the library. - - -# Additional typeclasses on measurable spaces - -Some results in probability theory require the sigma-algebra to be the Borel sigma-algebra, generated by the open sets. For example, with the Borel sigma-algebra the open sets are measurable and continuous functions are measurable. -For that we first need `Ω` to be a topological space and we then need to add a `[BorelSpace Ω]` variable. -```lean -variable {Ω : Type*} [MeasurableSpace Ω] [TopologicalSpace Ω] [BorelSpace Ω] -``` - -For properties related to conditional distributions, it is often convenient or necessary to work in a standard Borel space (a measurable space arising as the Borel sets of some Polish topology). See the `StandardBorelSpace` typeclass. -Note that a countable discrete measurable space is a standard Borel space, so there is no need to worry about that typeclass when doing discrete probability. diff --git a/LMLDocs/References.lean b/LMLDocs/References.lean deleted file mode 100644 index 78b8ba8a..00000000 --- a/LMLDocs/References.lean +++ /dev/null @@ -1,17 +0,0 @@ -/- -Copyright (c) 2026 Rémy Degenne. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne --/ -import VersoManual -open Verso.Genre.Manual - -namespace Docs - -def degenne2025markov : ArXiv where - title := inlines!"Markov kernels in Mathlib's probability library" - authors := #[inlines!"Rémy Degenne"] - year := 2025 - id := "2510.04070" - -end Docs diff --git a/LMLDocs/static_files/LigaMenlo-Regular.ttf b/LMLDocs/static_files/LigaMenlo-Regular.ttf deleted file mode 100644 index b1ca21e2..00000000 Binary files a/LMLDocs/static_files/LigaMenlo-Regular.ttf and /dev/null differ diff --git a/LMLDocs/static_files/favicon.svg b/LMLDocs/static_files/favicon.svg deleted file mode 100644 index ea497ae3..00000000 --- a/LMLDocs/static_files/favicon.svg +++ /dev/null @@ -1 +0,0 @@ -RealFaviconGeneratorhttps://realfavicongenerator.net \ No newline at end of file diff --git a/LMLDocs/static_files/scripts.js b/LMLDocs/static_files/scripts.js deleted file mode 100644 index 64c37a8d..00000000 --- a/LMLDocs/static_files/scripts.js +++ /dev/null @@ -1,23 +0,0 @@ -window.addEventListener('load', function () { - document.querySelectorAll('.has-info, .warning').forEach(function (el) { - el.classList.remove('has-info', 'warning'); - - el.querySelectorAll('span.hover-container').forEach(function (hoverSpan) { - hoverSpan.remove(); - }); - }); - - document.querySelectorAll('p').forEach(function (p) { - if (p.querySelector('img')) { - p.setAttribute('align', 'center'); - } - }); - - document.querySelectorAll('a[href]').forEach(function (link) { - const url = new URL(link.href, window.location.href); - if (url.hostname !== window.location.hostname) { - link.setAttribute('target', '_blank'); - link.setAttribute('rel', 'noopener noreferrer'); - } - }); -}); diff --git a/LMLDocs/static_files/style.css b/LMLDocs/static_files/style.css deleted file mode 100644 index b329089b..00000000 --- a/LMLDocs/static_files/style.css +++ /dev/null @@ -1,57 +0,0 @@ -:root { - --accent: #d65d5d; - --accent-compl: #e8a0a0; - --background: #fef9f9; - --background-lighter: #fefcfc; -} - -@font-face { - font-family: "LigaMenlo"; - src: url("LigaMenlo-Regular.ttf"); -} - -body { - text-align: justify; - background-color: var(--background); -} - -p a:visited, -p a:link { - text-decoration: none; - color: var(--accent); -} - -p a:hover { - text-decoration: underline; -} - -.toc { - background-color: var(--background-lighter); -} - -.keyword { - color: var(--accent) !important; -} - -.hl.lean .token.binding-hl, -.hl.lean .literal.string:hover, -.hl.lean .token.typed:hover { - background-color: var(--accent-compl) !important; - border-radius: 2px !important; -} - -.block { - background-color: var(--background-lighter); - padding: 0.4em; - border: 2px solid black; - border-radius: 0.5em; -} - -.tippy-box[data-theme~='lean'] { - background-color: var(--background-lighter) !important; -} - -code { - font-family: "LigaMenlo"; - font-variant-ligatures: normal; -} diff --git a/LMLTutorial/Front.lean b/LMLTutorial/Front.lean index 8020ee3e..3bdb0d89 100644 --- a/LMLTutorial/Front.lean +++ b/LMLTutorial/Front.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ import LMLTutorial.Pages.BasicProbability import LMLTutorial.Pages.DefiningAlgorithm import LMLTutorial.Pages.Installation diff --git a/LMLTutorial/Tutorial.lean b/LMLTutorial/Tutorial.lean index 760de515..ae5cf8ee 100644 --- a/LMLTutorial/Tutorial.lean +++ b/LMLTutorial/Tutorial.lean @@ -1,7 +1,14 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ import VersoManual - import LMLTutorial.Front +set_option linter.style.header false +set_option linter.style.setOption false + open Verso.Genre.Manual Verso.Output.Html def extraHead : Array Verso.Output.Html := #[ diff --git a/LMLTutorial/static_files/style.css b/LMLTutorial/static_files/style.css index b329089b..5c09270a 100644 --- a/LMLTutorial/static_files/style.css +++ b/LMLTutorial/static_files/style.css @@ -3,6 +3,7 @@ --accent-compl: #e8a0a0; --background: #fef9f9; --background-lighter: #fefcfc; + --verso-content-max-width: 60rem; } @font-face { diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean index 68f8c297..90057837 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithm.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean @@ -43,9 +43,11 @@ variable {𝓐 𝓨 Ω : Type*} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : Measurab structure Algorithm (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where /-- Policy or sampling rule: distribution of the next action. -/ policy : (n : ℕ) → Kernel (Iic n → 𝓐 × 𝓨) 𝓐 + /-- The policy is a Markov kernel. -/ [h_policy : ∀ n, IsMarkovKernel (policy n)] /-- Distribution of the first action. -/ p0 : Measure 𝓐 + /-- The first action distribution is a probability measure. -/ [hp0 : IsProbabilityMeasure p0] instance (alg : Algorithm 𝓐 𝓨) (n : ℕ) : IsMarkovKernel (alg.policy n) := alg.h_policy n @@ -53,6 +55,7 @@ instance (alg : Algorithm 𝓐 𝓨) : IsProbabilityMeasure alg.p0 := alg.hp0 /-- An algorithm with observations in `𝓧 × 𝓨` obtained from an algorithm with observations in `𝓨` by ignoring the `𝓧` component of each observation. -/ +@[simps] def Algorithm.prodLeft (𝓧 : Type*) [MeasurableSpace 𝓧] (alg : Algorithm 𝓐 𝓨) : Algorithm 𝓐 (𝓧 × 𝓨) where policy n := (alg.policy n).comap (fun h i ↦ ((h i).1, (h i).2.2)) (by fun_prop) @@ -62,9 +65,11 @@ def Algorithm.prodLeft (𝓧 : Type*) [MeasurableSpace 𝓧] (alg : Algorithm structure Environment (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where /-- Distribution of the next observation as function of the past history. -/ feedback : (n : ℕ) → Kernel ((Iic n → 𝓐 × 𝓨) × 𝓐) 𝓨 + /-- The feedback kernels are Markov kernels. -/ [h_feedback : ∀ n, IsMarkovKernel (feedback n)] /-- Distribution of the first observation given the first action. -/ ν0 : Kernel 𝓐 𝓨 + /-- The initial observation kernel is a Markov kernel. -/ [hp0 : IsMarkovKernel ν0] instance (env : Environment 𝓐 𝓨) (n : ℕ) : IsMarkovKernel (env.feedback n) := env.h_feedback n @@ -78,6 +83,9 @@ def stepKernel (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : alg.policy n ⊗ₖ env.feedback n deriving IsMarkovKernel +lemma stepKernel_def (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : + stepKernel alg env n = alg.policy n ⊗ₖ env.feedback n := rfl + @[simp] lemma fst_stepKernel (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : (stepKernel alg env n).fst = alg.policy n := by @@ -128,12 +136,19 @@ by an algorithm interacting with an environment. -/ structure IsAlgEnvSeq (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (P : Measure Ω) [IsFiniteMeasure P] : Prop where + /-- The action sequence is measurable. -/ measurable_action n : Measurable (A n) := by fun_prop + /-- The feedback sequence is measurable. -/ measurable_feedback n : Measurable (Y n) := by fun_prop + /-- The first action has the correct law. -/ hasLaw_action_zero : HasLaw (fun ω ↦ (A 0 ω)) alg.p0 P + /-- The first feedback has the correct conditional distribution. -/ hasCondDistrib_feedback_zero : HasCondDistrib (Y 0) (A 0) env.ν0 P + /-- The next action has the correct conditional distribution given the history. -/ hasCondDistrib_action n : HasCondDistrib (A (n + 1)) (IsAlgEnvSeq.hist A Y n) (alg.policy n) P + /-- The next feedback has the correct conditional distribution given the history and + next action. -/ hasCondDistrib_feedback n : HasCondDistrib (Y (n + 1)) (fun ω ↦ (IsAlgEnvSeq.hist A Y n ω, A (n + 1) ω)) (env.feedback n) P @@ -143,12 +158,19 @@ by an algorithm interacting with an environment. -/ structure IsAlgEnvSeqUntil (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (P : Measure Ω) [IsFiniteMeasure P] (N : ℕ) : Prop where + /-- The action sequence is measurable. -/ measurable_action n : Measurable (A n) := by fun_prop + /-- The feedback sequence is measurable. -/ measurable_feedback n : Measurable (Y n) := by fun_prop + /-- The first action has the correct law. -/ hasLaw_action_zero : HasLaw (fun ω ↦ (A 0 ω)) alg.p0 P + /-- The first feedback has the correct conditional distribution. -/ hasCondDistrib_feedback_zero : HasCondDistrib (Y 0) (A 0) env.ν0 P + /-- The next action has the correct conditional distribution given the history. -/ hasCondDistrib_action n (hn : n < N) : HasCondDistrib (A (n + 1)) (IsAlgEnvSeq.hist A Y n) (alg.policy n) P + /-- The next feedback has the correct conditional distribution given the history and + next action. -/ hasCondDistrib_feedback n (hn : n < N) : HasCondDistrib (Y (n + 1)) (fun ω ↦ (IsAlgEnvSeq.hist A Y n ω, A (n + 1) ω)) (env.feedback n) P diff --git a/lake-manifest.json b/lake-manifest.json index 057ce787..f2191ef8 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "4c6b02ee232211811f9ad1c148ac336122e256d7", + "rev": "a9c31d529b159723ab35371c7e9ee0896d6f2c68", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -115,7 +115,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a86770a5eba721c8554d1d7fce741bc4dde3bb61", + "rev": "0bd508e8362f56d4a05cbf63614d4c97db954041", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index 5b8e48a9..8533ac23 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -26,16 +26,7 @@ name = "LeanMachineLearning" name = "LMLTutorial" globs = ["LMLTutorial.*"] -[[lean_lib]] -name = "LMLDocs" -globs = ["LMLDocs.*"] - [[lean_exe]] name = "tutorial" srcDir = "LMLTutorial/" root = "Tutorial" - -[[lean_exe]] -name = "docs" -srcDir = "LMLDocs/" -root = "Docs" diff --git a/scripts/build_docs.sh b/scripts/build_docs.sh index 3939150e..260efac2 100755 --- a/scripts/build_docs.sh +++ b/scripts/build_docs.sh @@ -7,13 +7,6 @@ lake exe tutorial --output LMLTutorial/_out/site mkdir -p LMLTutorial/_out/site/html-multi/static cp LMLTutorial/static_files/* LMLTutorial/_out/site/html-multi/static -# Build docs -lake exe docs --output LMLDocs/_out/site -mkdir -p LMLDocs/_out/site/html-multi/static -cp LMLDocs/static_files/* LMLDocs/_out/site/html-multi/static - # Copy outputs to home_page mkdir -p home_page/tutorial cp -r LMLTutorial/_out/site/html-multi/* home_page/tutorial -mkdir -p home_page/defdocs -cp -r LMLDocs/_out/site/html-multi/* home_page/defdocs