update

Author: avigad

.devcontainer/Dockerfile

@@ -0,0 +1,8 @@
+FROM mcr.microsoft.com/devcontainers/base:jammy
+
+USER vscode
+WORKDIR /home/vscode
+
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+ENV PATH="/home/vscode/.elan/bin:${PATH}"

.devcontainer/devcontainer.json

@@ -0,0 +1,15 @@
+{
+  "name": "LAMR dev container",
+
+  "build": {
+    "dockerfile": "Dockerfile"
+  },
+
+  "onCreateCommand": "echo \"Downloading the Lean 4 mathematical library...\" && lake exe cache get! && lake build && echo \"Finished setup! Open a file using the Explorer in the top-left of your screen.\"",
+
+  "customizations": {
+    "vscode" : {
+      "extensions" : [ "leanprover.lean4" ]
+    }
+  }
+}

.docker/gitpod/Dockerfile

@@ -0,0 +1,37 @@
+# This is the Dockerfile for `leanprovercommunity/mathlib:gitpod`.
+
+# gitpod doesn't support multiple FROM statements, (or rather, you can't copy from one to another)
+# so we just install everything in one go
+FROM ubuntu:jammy
+
+USER root
+
+RUN apt-get update && apt-get install sudo git curl git bash-completion -y && apt-get clean
+
+RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
+    # passwordless sudo for users in the 'sudo' group
+    && sed -i.bkp -e 's/%sudo\s\+ALL=(ALL\(:ALL\)\?)\s\+ALL/%sudo ALL=NOPASSWD:ALL/g' /etc/sudoers
+USER gitpod
+WORKDIR /home/gitpod
+
+SHELL ["/bin/bash", "-c"]
+
+# gitpod bash prompt
+RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[00m\]\$(__git_ps1 \" (%s)\") $ '" ; } >> .bashrc
+
+# install elan
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+# install whichever toolchain mathlib is currently using
+RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/hrmacbeth/math2001/main/lean-toolchain)
+
+ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:${PATH}"
+
+# fix the infoview when the container is used on gitpod:
+ENV VSCODE_API_VERSION="1.50.0"
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true
+
+# run sudo once to suppress usage info
+RUN sudo echo finished

.gitignore

@@ -15,6 +15,7 @@
 ## Build directories
 build/
 _build/
+.lake/
 
 ## Intermediate documents:
 *.dvi
@@ -26,7 +27,7 @@ _build/
 # *.pdf
 
 ## Generated if empty string is given at "Please type another file name for output:"
-.pdf
+*.pdf
 
 ## Bibliography auxiliary files (bibtex/biblatex/biber):
 *.bbl

.gitpod.Dockerfile

@@ -1,10 +1,11 @@
 image:
-  file: .gitpod.Dockerfile
-
-tasks:
-  - init: |
-      lake build
+  file: .docker/gitpod/Dockerfile
 
 vscode:
   extensions:
     - leanprover.lean4
+
+tasks:
+  - init: |
+      lake exe cache get && lake build LAMR
+

.gitpod.yml

@@ -0,0 +1,35 @@
+{
+    "files.exclude": {
+        "**/.git": true,
+        "**/.DS_Store": true,
+        "**/*.olean": true,
+        "**/.DS_yml": true,
+        "**/.gitpod.yml": true,
+        "**/.vscode": true,
+        ".devcontainer.json": true,
+        ".docker": true,
+        "build": true,
+        "html": true,
+        "lake-packages": true,
+        ".gitignore": true,
+        "lake-manifest.json": true,
+        "lakefile.lean": true,
+        "lean-toolchain": true,
+	    ".lake": true,
+	    ".devcontainer": true
+    },
+    "editor.minimap.enabled": false,
+    "editor.acceptSuggestionOnEnter": "off",
+    "scm.diffDecorationsGutterVisibility": "hover",
+    "editor.semanticHighlighting.enabled": true,
+    "editor.semanticTokenColorCustomizations": {
+        "[Default Light+]": {"rules": {"variable": "#1a31da"}}
+    },
+    "editor.unicodeHighlight.nonBasicASCII": false,
+    "editor.unicodeHighlight.ambiguousCharacters": false,
+    "editor.fontLigatures": true,
+    "files.trimTrailingWhitespace": true,
+    "files.trimFinalNewlines": true,
+    "lean4.infoview.emphasizeFirstGoal": true,
+    "lean4.infoview.showExpectedType": false
+}

.vscode/settings.json

@@ -1,4 +1,3 @@
-import Mathlib
 import LAMR.Util.Propositional
 import LAMR.Util.FirstOrder
 import LAMR.Util.DisjointSet

LAMR.lean

@@ -32,13 +32,13 @@ def List.toLinearExp (l : List (String × Int)) : LinearExp := l.toHashMap
 instance : Coe (List (String × Int)) LinearExp := ⟨List.toLinearExp⟩
 
 instance : ToString LinearExp := ⟨fun linexp =>
-  String.intercalate " + " $ linexp.toList.map (fun (s, i) => (ToString.toString i ++ "*" ++ s))⟩
+  String.intercalate " + " <| linexp.toList.map (fun (s, i) => (ToString.toString i ++ "*" ++ s))⟩
 
 def ex1 : LinearExp := [("x", 3), ("y", -2), ("z", 4)]
 def ex2 : LinearExp := [("x", 4), ("y", 2), ("w", -1), ("v", 3)]
 
-#eval toString $ ex1
-#eval toString $ ex2
+#eval toString ex1
+#eval toString ex2
 
 
 /--
@@ -59,13 +59,13 @@ def linearCombination (a : Int) (u : LinearExp) (b : Int) (v : LinearExp) : Line
       result := result.insert t (b * j)
   result
 
-#eval toString $ linearCombination 1 ex1 1 ex2
-#eval toString $ linearCombination 1 ex1 (-1) ex1
-#eval toString $ linearCombination 2 ex1 (-3) ex2
+#eval toString <| linearCombination 1 ex1 1 ex2
+#eval toString <| linearCombination 1 ex1 (-1) ex1
+#eval toString <| linearCombination 2 ex1 (-3) ex2
 
 -- checks whether an expression is empty
 #eval ex1.isEmpty
-#eval HashMap.isEmpty $ linearCombination 1 ex1 (-1) ex1
+#eval HashMap.isEmpty <| linearCombination 1 ex1 (-1) ex1
 
 -- you can erase a term from an expression
 #eval let ex' : LinearExp := ex1.erase "x"
@@ -191,8 +191,8 @@ def wikipedia_constraints : List LinearExp :=
     [("one", -7), ("x",  1), ("y", -5), ("z",  2)],
     [("one", 12), ("x",  3), ("y", -2), ("z", -6)] ]
 
-#eval toString $ sortGtConstraints "x" wikipedia_constraints
-#eval toString $ elimVarGtConstraints "x" wikipedia_constraints
+#eval toString <| sortGtConstraints "x" wikipedia_constraints
+#eval toString <| elimVarGtConstraints "x" wikipedia_constraints
 
 /-
 Given a pair `eq, gts`, we want to eliminate all the variables to determine whether it is

LAMR/Examples/decision_procedures_for_first_order_logic/FourierMotzkin.lean

@@ -133,7 +133,7 @@ def World.toArray (world : World) : Array (Array (Option Object)) := Id.run do
   for obj in world do
     assert! obj.row < 8
     assert! obj.col < 8
-    arr := arr.set! obj.row $ arr[obj.row]!.set! obj.col (some obj)
+    arr := arr.set! obj.row <| arr[obj.row]!.set! obj.col (some obj)
   arr
 
 instance : ToString World :=
@@ -148,7 +148,7 @@ instance : ToString World :=
       s := s ++ "\n" ++ rowDashes ++ "\n"
     s⟩
 
-def World.show (world : World) : IO Unit := do IO.print $ toString world
+def World.show (world : World) : IO Unit := do IO.print <| toString world
 
 /-
 Implement the language