Merge pull request #41 from leanprover-community/lean-pr-testing-3226

feat: adaptations for leanprover/lean4#3226

.github/workflows/build.yml

@@ -59,17 +59,10 @@ jobs:
         if: github.ref_type == 'tag'
         uses: softprops/action-gh-release@v1
 
-      # TODO: replace with just `lake upload $RELEASE_TAG` when lean4#2713 is fixed
-      # References:
-      # https://docs.github.com/en/actions/learn-github-actions/contexts#runner-context
-      # https://stackoverflow.com/questions/8766730/tar-command-in-mac-os-x-adding-hidden-files-why
       - name: Upload release archive
         if: github.ref_type == 'tag'
-        # All our runners are 64-bit ¯\_(ツ)_/¯
         run: |
-          export COPYFILE_DISABLE=true
-          tar -c -z -f ./${LEAN_OS}-64.tar.gz -C ./.lake/build .
-          gh release upload ${RELEASE_TAG} ./${LEAN_OS}-64.tar.gz
+          lake upload $RELEASE_TAG
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           RELEASE_TAG: ${{ github.ref_name }}

ProofWidgets/Compat.lean

@@ -17,7 +17,7 @@ def ExprWithCtx.runMetaM (e : ExprWithCtx) (x : Expr → MetaM α) : IO α :=
 
 def ExprWithCtx.save (e : Expr) : MetaM ExprWithCtx :=
   return {
-    ci := ← ContextInfo.save
+    ci := { ← CommandContextInfo.save with }
     lctx := ← getLCtx
     expr := e
   }

ProofWidgets/Demos/LazyComputation.lean

@@ -50,7 +50,7 @@ syntax (name := makeRunnerTac) "make_runner" : tactic
     -- Store the continuation and monad context.
     let props : RunnerWidgetProps := {
       k := ⟨{
-        ci := (← ContextInfo.save)
+        ci := { ← CommandContextInfo.save with }
         lctx := (← getLCtx)
         k := x
       }⟩}

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "ee49cf8fada1bf5a15592c399a925c401848227f",
+   "rev": "276953b13323ca151939eafaaec9129bf7970306",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.lean

@@ -3,6 +3,7 @@ open Lake DSL System
 
 package proofwidgets where
   preferReleaseBuild := true
+  buildArchive := "ProofWidgets4.tar.gz"
 
 lean_lib ProofWidgets
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.6.0-rc1