Merge remote-tracking branch 'upstream/main' into mvcgen-tutorial

Author: david-christiansen

.github/workflows/ci.yml

@@ -131,7 +131,7 @@ jobs:
             rm parse_times.py
           else
             echo "No build log found" >> $GITHUB_STEP_SUMMARY
-          fi            
+          fi
 
       - name: Save cache for .lake
         uses: actions/cache/save@v4
@@ -149,6 +149,10 @@ jobs:
         run: |
           lake --quiet exe generate-manual --depth 2 --with-word-count "words.txt" --verbose --without-html-single
 
+      - name: Check Manual Examples are Isolated
+        run: |
+          scripts/check-examples-isolated.sh
+
       - name: Generate proofreading HTML
         if: github.event_name == 'pull_request'
         id: generate
@@ -380,4 +384,3 @@ jobs:
         run: |
           cd _out/html-multi/-verso-search
           tsc --noEmit -p jsconfig.json
-

.github/workflows/overlay.yml

@@ -0,0 +1,47 @@
+name: Apply Overlays
+
+on:
+  workflow_run:
+    workflows: ["Deploy Tagged Version"]
+    types:
+      - completed
+
+  push:
+    branches:
+      - 'deploy'
+
+  workflow_dispatch:
+
+jobs:
+  apply-overlays:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write  # This allows pushing to the repository
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.10'
+
+      - name: Configure Git
+        # These values are recommended at:
+        #   https://github.com/actions/checkout?tab=readme-ov-file#push-a-commit-using-the-built-in-token
+        run: |
+          git config --global user.name "github-actions[bot]"
+          git config --global user.email "41898282+github-actions[bot]@users.noreply.github.com"
+          git fetch origin deploy:deploy
+          git fetch origin postdeploy:postdeploy
+
+      - name: Run overlay script
+        run: |
+          echo "Adding overlays to predeploy"
+          # -B to prevent creation of __pycache__ directory
+          # which would get committed due to lack of .gitignore
+          python -B deploy/overlay.py . deploy postdeploy
+
+      - name: Push deploy branch
+        run: |
+          git push origin postdeploy

.github/workflows/release-tag.yml

@@ -15,12 +15,12 @@ jobs:
         uses: actions/checkout@v4
         with:
           fetch-depth: 0  # Fetch all history for all tags and branches
-      
+
       - name: Set up Python
         uses: actions/setup-python@v5
         with:
           python-version: '3.10'
-      
+
       - name: Extract version from tag
         id: get_version
         run: |
@@ -107,13 +107,11 @@ jobs:
         run: |
           # The tag name is simply GITHUB_REF_NAME
           TAG_NAME=$GITHUB_REF_NAME
-          echo "Deploying from tag: '$TAG_NAME'"
-          
+          echo "Making deployment from tag: '$TAG_NAME'"
+
 
           python deploy/release.py html/html-multi "$VERSION" deploy
 
       - name: Push deploy branch
         run: |
           git push origin deploy
-          
-        

.github/workflows/upload-snapshots.yml

@@ -1,13 +1,13 @@
-name: "Deploy the 'deploy' branch"
+name: "Deploy the 'postdeploy' branch"
 on:
   workflow_run:
-    workflows: ["Deploy Tagged Version"]
+    workflows: ["Apply Overlays"]
     types:
       - completed
 
   push:
     branches:
-      - 'deploy'
+      - 'postdeploy'
 
   workflow_dispatch:
 
@@ -18,17 +18,17 @@ jobs:
     if: ${{ github.event_name != 'workflow_run' || github.event.workflow_run.conclusion == 'success' }}
     steps:
 
-      - name: Checkout deploy branch
+      - name: Checkout postdeploy branch
         uses: actions/checkout@v4
         with:
-          ref: 'deploy'
+          ref: 'postdeploy'
 
-      - name: Upload the current state of the deploy branch
+      - name: Upload the current state of the postdeploy branch
         id: deploy-release
         uses: nwtgck/[email protected]
         with:
           publish-dir: '.'
-          production-branch: deploy
+          production-branch: postdeploy
           production-deploy: true
           github-token: ${{ secrets.GITHUB_TOKEN }}
           deploy-message: |

.vale/scripts/rewrite_html.py

@@ -7,6 +7,18 @@
 
 def process_html_file(filepath, output_filepath):
     """Reads an HTML file, removes 'QA' from headers, and writes the result to the output path."""
+
+    # We exclude release notes. Before
+    # https://github.com/leanprover/reference-manual/pull/599 we generated one
+    # block for each release notes document which had class="no-vale" on it.
+    # However, it's currently not easy to add any attributes to verso parts,
+    # which https://github.com/leanprover/reference-manual/pull/599 adds, hence
+    # the current workaround here.
+    #
+    # Reconsider this if https://github.com/leanprover/verso/issues/561 is resolved.
+    if "/releases/" in filepath:
+        return
+
     with open(filepath, 'r', encoding='utf-8') as file:
         soup = BeautifulSoup(file, 'html.parser')
 

.vale/styles/config/ignore/terms.txt

@@ -217,4 +217,5 @@ upvote
 VC
 VCs
 walkthrough
+workspace's
 zulip

ExtractExplanationExamples.lean

@@ -81,7 +81,7 @@ where
       IO Highlighted :=
     let termElab : TermElabM Highlighted := do
       let mut hls := Highlighted.empty
-      let mut lastPos : String.Pos := 0
+      let mut lastPos : String.Pos.Raw := 0
       for cmd in cmds do
         let hl ← highlightIncludingUnparsed cmd nonSilentMsgs cmdState.infoState.trees [] lastPos
         hls := hls ++ hl

Main.lean

@@ -6,6 +6,7 @@ Author: David Thrane Christiansen
 import Manual
 import Manual.Meta
 import VersoManual
+import Manual.ExtractExamples
 
 open Verso.Genre.Manual
 open Verso.Genre.Manual.InlineLean
@@ -32,7 +33,7 @@ def staticCss := {{
   }}
 
 def main :=
-  manualMain (%doc Manual) (config := config)
+  manualMain (%doc Manual) (config := config) (extraSteps := [extractExamples])
 where
   config := Config.addSearch <| Config.addKaTeX {
     extraFiles := [("static", "static")],

Manual.lean

@@ -30,6 +30,7 @@ import Manual.Releases
 import Manual.Namespaces
 import Manual.Runtime
 import Manual.ModuleSystem
+import Manual.SupportedPlatforms
 
 open Verso.Genre Manual
 open Verso.Genre.Manual.InlineLean
@@ -144,6 +145,8 @@ Overview of the standard library, including types from the prelude and those tha
 
 {include 0 Manual.Releases}
 
+{include 0 Manual.SupportedPlatforms}
+
 # Index
 %%%
 number := false
@@ -164,6 +167,9 @@ file := some "the-index"
 
 :::progress
 ```namespace
+ByteArray
+ByteArray.Iterator
+ByteSlice
 List
 Int
 IntCast
@@ -206,6 +212,7 @@ LawfulFunctor
 LawfulApplicative
 LawfulMonad
 LawfulBEq
+ReflBEq
 EquivBEq
 LawfulHashable
 Id
@@ -219,7 +226,13 @@ EStateM.Result
 EStateM.Backtrackable
 String
 Substring
+String.Slice
+String.Slice.Pos
+String.Pattern
+String.Pos.Raw
 String.Pos
+String.ValidPos
+String.Iterator
 Char
 Nat
 Lean.Elab.Tactic
@@ -405,6 +418,43 @@ Substring.takeRightWhileAux
 Substring.takeWhileAux
 ```
 
+```exceptions
+String.Pos.Raw.ctorIdx
+String.Pos.Raw.extract.go₁
+String.Pos.Raw.extract.go₂
+String.Pos.Raw.mk.noConfusion
+String.Pos.Raw.utf8GetAux
+String.Pos.Raw.utf8GetAux?
+String.Pos.Raw.utf8PrevAux
+String.Pos.Raw.utf8SetAux
+```
+
+```exceptions
+String.Slice.ctorIdx
+String.Slice.hash
+String.Slice.instDecidableEqPos.decEq
+String.Slice.instInhabitedByteIterator.default
+String.Slice.instInhabitedPosIterator.default
+String.Slice.instInhabitedRevPosIterator.default
+String.Slice.instInhabitedRevSplitIterator.default
+String.Slice.instInhabitedSplitInclusiveIterator.default
+String.Slice.instInhabitedSplitIterator.default
+String.Slice.lines.lineMap
+String.Slice.mk.noConfusion
+```
+
+```exceptions
+String.Slice.Pos.ctorIdx
+String.Slice.Pos.mk.noConfusion
+String.Slice.Pos.prevAux
+String.Slice.Pos.prevAux.go
+```
+
+```exceptions
+String.ValidPos.ctorIdx
+String.ValidPos.mk.noConfusion
+```
+
 ```exceptions
 Char.ofNatAux
 Char.quoteCore
@@ -436,6 +486,34 @@ BitVec.reduceShiftWithBitVecLit
 BitVec.reduceUnary
 ```
 
+```exceptions
+ByteArray.ctorIdx
+ByteArray.findFinIdx?.loop
+ByteArray.findIdx?.loop
+ByteArray.foldlM.loop
+ByteArray.foldlMUnsafe
+ByteArray.foldlMUnsafe.fold
+ByteArray.forIn.loop
+ByteArray.forInUnsafe
+ByteArray.forInUnsafe.loop
+ByteArray.hash
+ByteArray.instBEq.beq
+ByteArray.instInhabitedIterator.default
+ByteArray.mk.noConfusion
+ByteArray.mkIterator
+ByteArray.toList.loop
+ByteArray.utf8Decode?.go
+ByteArray.utf8DecodeChar?.assemble₁
+ByteArray.utf8DecodeChar?.assemble₂
+ByteArray.utf8DecodeChar?.assemble₂Unchecked
+ByteArray.utf8DecodeChar?.assemble₃
+ByteArray.utf8DecodeChar?.assemble₃Unchecked
+ByteArray.utf8DecodeChar?.assemble₄
+ByteArray.utf8DecodeChar?.assemble₄Unchecked
+ByteArray.utf8DecodeChar?.isInvalidContinuationByte
+ByteArray.utf8DecodeChar?.parseFirstByte
+```
+
 ```exceptions
 Quot.indep
 Quot.lcInv