wip

.github/workflows/compile.yml

@@ -8,8 +8,10 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v2
+
       - name: Compile bundle
-        uses: pi-base/compile@releases/v1
+        # uses: pi-base/compile@releases/v1
+        uses: pi-base/compile@db9b28568288b04d8da4c0a01e5c036df0adbb16
         with:
           out: bundle.json
 
@@ -26,7 +28,7 @@ jobs:
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
           echo "$HOME/.elan/bin/" >> $GITHUB_PATH
 
-      - name: Setup lake cache
+      - name: Build dependencies
         shell: bash
         run: |
           cd .lean 
@@ -37,7 +39,7 @@ jobs:
         shell: bash
         run: |
           cd .lean 
-          lake exec pibase extract || true
+          lake exec pibase extract ../bundle.json > ../bundle.extra.json
 
       - name: Persist bundle as artifact
         uses: actions/[email protected]
@@ -46,7 +48,7 @@ jobs:
           path: bundle.json
       - name: Upload bundle to S3
         run: |
-          aws s3 cp --acl public-read bundle.json s3://pi-base-bundles/${GITHUB_REF:-unknown}.json
+          aws s3 cp --acl public-read bundle.extra.json s3://pi-base-bundles/${GITHUB_REF:-unknown}.json
         env:
           AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}
           AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }}

.lean/Main.lean

@@ -6,17 +6,34 @@ import Cli
 
 open Lean Cli
 
-unsafe def runExtractCmd (_ : Parsed) : IO UInt32 := do
-  PiBase.findProperties $ fun json => do
-    IO.println json
-  return 0
+unsafe def runExtractCmd (p : Parsed) : IO UInt32 := do
+  let bundlePath := match p.positionalArgs[0]? with
+    | some a => a.value
+    | _ => "bundle.json"
+  let raw <- Json.parse <$> IO.FS.readFile bundlePath
+  match raw with
+    | Except.error err => do
+      IO.println err
+      return 1
+    | Except.ok (Json.obj bundle) => do
+      PiBase.findProperties $ fun lean => do
+        -- TODO - non-partial version
+        let merged := Json.setObjVal! (Json.obj bundle) "lean" lean
+        IO.println merged
+      return 0
+    | Except.ok _ => do
+      IO.println "Bundle is not an object"
+      return 1
 
 unsafe def runVerifyCmd (_ : Parsed) : IO UInt32 := do
   return 0
 
 unsafe def extract := `[Cli|
   extract VIA runExtractCmd;
   "extract ."
+
+  ARGS:
+    input : String;      "Path to the input bundle file"
 ]
 
 unsafe def runPiBaseCmd (p : Parsed) : IO UInt32 := do

.lean/lake-manifest.json

@@ -23,7 +23,7 @@
     "rev": "ac00de12d4cdf0e1ef8927c6fe6fd14020a390c0",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": null,
+    "inputRev?": "ac00de12d4cdf0e1ef8927c6fe6fd14020a390c0",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover/std4",

.lean/lakefile.lean

@@ -10,7 +10,7 @@ require CMark from git
   "https://github.com/xubaiw/CMark.lean" @ "main"
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
+  "https://github.com/leanprover-community/mathlib4.git" @ "ac00de12d4cdf0e1ef8927c6fe6fd14020a390c0"
 
 lean_lib PiBase
 

properties/P000001.md

@@ -7,6 +7,7 @@ aliases:
 refs:
   - doi: 10.1007/978-1-4612-6290-9
     name: Counterexamples in Topology
+mathlib: T0Space
 ---
 
 Given any two distinct points, there is an open set containing one but not the other.

properties/P000002.md

@@ -7,6 +7,7 @@ aliases:
 refs:
   - doi: 10.1007/978-1-4612-6290-9
     name: Counterexamples in Topology
+mathlib: T1Space
 ---
 
 Given any two distinct points, each has an open set not containing the other.

properties/P000003.md

@@ -7,6 +7,7 @@ aliases:
 refs:
   - doi: 10.1007/978-1-4612-6290-9
     name: Counterexamples in Topology
+mathlib: T2Space
 ---
 
 Given any two distinct points $a$ and $b$, there are disjoint open sets $O_a$ and $O_b$ containing $a$ and $b$, respectively.

properties/P000004.md

@@ -12,12 +12,13 @@ refs:
     name: Counterexamples in Topology
   - wikipedia: Urysohn_and_completely_Hausdorff_spaces
     name: Urysohn and completely Hausdorff spaces
+mathlib: T25Space
 ---
 
 Distinct points are separated by closed neighborhoods.
 In other words, given any two distinct points $a$ and $b$, there are open sets $O_a$ and $O_b$ containing $a$ and $b$,
 respectively, such that $cl(O_a)$ and $cl(O_b)$ are disjoint.
 
 Defined as "Urysohn" in 14F of {{mr:MR2048350}}.
-Defined as "completely Hausdorff" and \(T_{2\frac{1}{2}}\) on page 13 of
+Defined as "completely Hausdorff" and \(T\_{2\frac{1}{2}}\) on page 13 of
 {{doi:10.1007/978-1-4612-6290-9}}.

properties/P000005.md

@@ -7,9 +7,10 @@ aliases:
 refs:
   - mr: MR2048350
     name: General Topology (Willard)
+mathlib: T3Space
 ---
 
-A space which is both {P11} and {P3}. 
+A space which is both {P11} and {P3}.
 Equivalently, a space that is both {P11} and {P1}.
 
 Defined in 14.1 of {{mr:MR2048350}}.

properties/P000006.md

@@ -10,7 +10,8 @@ refs:
     name: General Topology (Willard)
   - wikipedia: Tychonoff_space
     name: Tychonoff space
+mathlib: T35Space
 ---
 
-A space which is both {P12} and {P3}. 
+A space which is both {P12} and {P3}.
 Equivalently, a space that is both {P12} and {P1}.

properties/P000007.md

@@ -7,9 +7,10 @@ aliases:
 refs:
   - mr: MR2048350
     name: General Topology (Willard)
+mathlib: T4Space
 ---
 
-A space which is both {P13} and {P3}. 
+A space which is both {P13} and {P3}.
 Equivalently, a space that is both {P13} and {P2}.
 
 Defined in 15.1 of {{mr:MR2048350}}.

properties/P000008.md

@@ -7,9 +7,10 @@ aliases:
 refs:
   - doi: 10.1007/978-1-4612-6290-9
     name: Counterexamples in Topology
+mathlib: T5Space
 ---
 
-A space which is both {P14} and {P3}. 
+A space which is both {P14} and {P3}.
 Equivalently, a space that is both {P14} and {P2}.
 
 Defined on page 12 of {{doi:10.1007/978-1-4612-6290-9}} as "completely normal".

properties/P000011.md

@@ -4,6 +4,7 @@ name: Regular
 refs:
   - mr: MR2048350
     name: General Topology (Willard)
+mathlib: RegularSpace
 ---
 
 A space in which a closed set and a point not contained in it

properties/P000012.md

@@ -2,18 +2,19 @@
 uid: P000012
 name: Completely regular
 aliases:
-- Uniformizable
+  - Uniformizable
 refs:
   - mr: MR2048350
     name: General Topology (Willard)
   - wikipedia: Uniform_space
     name: Uniform space on Wikipedia
+mathlib: CompletelyRegularSpace
 ---
 
-A space in which points and closed sets can be separated by a function. 
+A space in which points and closed sets can be separated by a function.
 
 Namely, given a closed set $A$ and a point $b \notin A$, there is a continuous function $f:X \rightarrow [0,1]$ such that $f(A) = \{0\}$ and $f(b)=1$.
 
 Defined in 14.8 of {{mr:MR2048350}}.
 
-Equivalently, the topology is induced by a uniformity.  See Theorem 38.2 in {{mr:MR2048350}} and {{wikipedia:Uniform_space}}.
+Equivalently, the topology is induced by a uniformity. See Theorem 38.2 in {{mr:MR2048350}} and {{wikipedia:Uniform_space}}.

theorems/T000266.md

@@ -5,9 +5,8 @@ if:
 then:
   P000090: true
 refs:
-- wikipedia: Alexandrov_topology
-  name: Alexandrov Topology on Wikipedia
-
+  - wikipedia: Alexandrov_topology
+    name: Alexandrov Topology on Wikipedia
 ---
 
 A topology on a finite set has only finitely many open sets.

theorems/T000308.md

@@ -6,7 +6,7 @@ if:
     - P000125: true
     - P000139: true
 then:
-  P000036: False
+  P000036: false
 ---
 
 By {P139} there is a singleton set $\{x\}$ open. By {P2} it is closed.