From 5c96cde613cc637bba0cd5366c57831f05af57d9 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Fri, 22 Dec 2023 06:06:48 -0500
Subject: [PATCH 1/6] chore: update lean toolchain

---
 Http/HeaderName.lean |  2 +-
 Http/URI.lean        |  9 +++--
 lake-manifest.json   | 82 +++++++++++++++++++++-----------------------
 lean-toolchain       |  2 +-
 4 files changed, 46 insertions(+), 49 deletions(-)

diff --git a/Http/HeaderName.lean b/Http/HeaderName.lean
index 236cd40..bec0df7 100644
--- a/Http/HeaderName.lean
+++ b/Http/HeaderName.lean
@@ -895,7 +895,7 @@ namespace Standard
 
 -- TODO: check if trie is faster than whatever leanc+llvm produce
 -- if you just pattern match on all the strings
-def trie := all.foldl (fun a b => a.insert b.toHeaderString b) (Lean.Parser.Trie.empty)
+def trie := all.foldl (fun a b => a.insert b.toHeaderString b) Lean.Data.Trie.empty
 def parse := trie.find?
 
 end HeaderName.Standard
diff --git a/Http/URI.lean b/Http/URI.lean
index 3ccc3a4..d89c7cc 100644
--- a/Http/URI.lean
+++ b/Http/URI.lean
@@ -31,7 +31,7 @@ def ofString (s : String) : Option Scheme :=
   else
     none
 
-instance : Inhabited Scheme := ⟨ofString "a" |>.get (by simp only)⟩
+instance : Inhabited Scheme := ⟨ofString "a" |>.get rfl⟩
 
 def HTTP := ofString "http" |>.get!
 def HTTPS := ofString "https" |>.get!
@@ -185,7 +185,7 @@ def Path.allowedSegChars : ByteArray :=
     else 0
   )
 
-@[simp] theorem Path.allowedSegChars_size : Path.allowedSegChars.size = 256 := by
+theorem Path.allowedSegChars_size : Path.allowedSegChars.size = 256 := by
   simp [ByteArray.size, allowedSegChars]
 
 def Path.pctEnc : Parser Char := do
@@ -200,8 +200,7 @@ def Path.parse : Parser Path := do
     token '/' *> (capture <| dropMany <|
       (tokenFilter (fun c =>
         if h : c.toNat < 256 then
-          have := by rw [←Path.allowedSegChars_size] at h; exact h
-          Path.allowedSegChars[c.toNat] > 0
+          Path.allowedSegChars[c.toNat]'(Path.allowedSegChars_size ▸ h) > 0
         else
           false
       )
@@ -237,4 +236,4 @@ def fromString? (s : String) : Option URI :=
     if ss.isEmpty then some u else none
   | _ => none
 
-#eval fromString? "https://api.github.com" |>.map (·.appendPath #["hi"])
+-- #eval fromString? "https://api.github.com" |>.map (·.appendPath #["hi"])
diff --git a/lake-manifest.json b/lake-manifest.json
index 1bff5b1..85e899d 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,43 +1,41 @@
-{"version": 5,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/fgdorais/lean4-parser",
-    "subDir?": null,
-    "rev": "2d59ec7dcd5e36ed2e2fc8ea9dd06abe957cdb76",
-    "opts": {},
-    "name": "Parser",
-    "inputRev?": "main",
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/gebner/quote4",
-    "subDir?": null,
-    "rev": "e75daed95ad1c92af4e577fea95e234d7a8401c1",
-    "opts": {},
-    "name": "Qq",
-    "inputRev?": "master",
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-    "subDir?": null,
-    "rev": "2491e781ae478b6e6f1d86a7157f1c58fc50f895",
-    "opts": {},
-    "name": "UnicodeBasic",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "54da53d93077d8bd1e3f0a9d318d50387fed1fd6",
-    "opts": {},
-    "name": "Std",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "ba5e5e3af519b4fc5221ad0fa4b2c87276f1d323",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": false}}]}
+ [{"url": "https://github.com/gebner/quote4",
+   "type": "git",
+   "subDir": null,
+   "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "ee49cf8fada1bf5a15592c399a925c401848227f",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "rev": "8603bb1d0d5edae780e3a85a0398fd83dbbb80a3",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-parser",
+   "type": "git",
+   "subDir": null,
+   "rev": "9af869c770afa8572e0c4854b0a3dd33c48ea735",
+   "name": "Parser",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "Http",
+ "lakeDir": ".lake"}
diff --git a/lean-toolchain b/lean-toolchain
index f0a6d66..3f21e50 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4:v4.5.0-rc1

From 7179376f5c97053630dcd43d7d5246c0687e4c9a Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Fri, 22 Dec 2023 09:16:05 -0500
Subject: [PATCH 2/6] fix: use Parser.Char.captureString

---
 Http/HeaderName.lean |  6 +++---
 Http/Headers.lean    |  5 +++--
 Http/Parser.lean     | 16 ++++++++--------
 Http/URI.lean        | 36 ++++++++++++++++++------------------
 lake-manifest.json   |  2 +-
 5 files changed, 33 insertions(+), 32 deletions(-)

diff --git a/Http/HeaderName.lean b/Http/HeaderName.lean
index bec0df7..2f31a8e 100644
--- a/Http/HeaderName.lean
+++ b/Http/HeaderName.lean
@@ -917,10 +917,10 @@ def ofHeaderString (s : String) :=
   | some n => standard n
   | none => custom ⟨s, _, by congr⟩
 
-end Http.HeaderName open Parser open Http.Parser
+end Http.HeaderName open Parser Char open Http.Parser
 namespace Http.HeaderName
 
 def parse : Parser HeaderName := do
-  let str ← capture <| dropMany1 (tokenFilter (fun c => Char.isAlphanum c ||
+  let str ← captureString <| dropMany1 (tokenFilter (fun c => Char.isAlphanum c ||
             c ∈ ['-', '_', '!', '#', '$', '%', '&', '|', '*', '+', '.', '^', '"', '\'', '`']))
-  return HeaderName.ofHeaderString str.toString
+  return HeaderName.ofHeaderString str.2.toString
diff --git a/Http/Headers.lean b/Http/Headers.lean
index e455fe2..11f3091 100644
--- a/Http/Headers.lean
+++ b/Http/Headers.lean
@@ -7,6 +7,7 @@ import Std
 import Http.Parser
 import Http.HeaderName
 
+open Parser Char
 open Http.Parser
 
 namespace Http
@@ -41,9 +42,9 @@ def parseHeader : Parser (HeaderName × String) := do
   ws
   let _ ← Parser.token ':'
   ws
-  let value ← capture <| Parser.dropMany <| Parser.tokenFilter (fun c => c != '\n')
+  let value ← captureString <| Parser.dropMany <| Parser.tokenFilter (fun c => c != '\n')
   ws
-  return (key, value.toString)
+  return (key, value.2.toString)
 
 def parse : Parser Headers := do
   let headers ← Array.foldl (λ map (k, v) => map.add k v) .empty <$>
diff --git a/Http/Parser.lean b/Http/Parser.lean
index 949ca2c..62f2a37 100644
--- a/Http/Parser.lean
+++ b/Http/Parser.lean
@@ -10,14 +10,14 @@ namespace Http
 nonrec abbrev Parser.Error := Parser.Error.Simple Substring Char
 nonrec abbrev Parser := Parser Parser.Error Substring Char
 
-def Parser.capture (p : Parser α) : Parser Substring := do
-  let p1 ← Parser.getPosition
-  let _ ← p
-  let p2 ← Parser.getPosition
-  return { (← StateT.get).stream with
-      startPos := p1
-      stopPos := p2
-    }
+-- def Parser.capture (p : Parser α) : Parser Substring := do
+--   let p1 ← Parser.getPosition
+--   let _ ← p
+--   let p2 ← Parser.getPosition
+--   return { (← StateT.get).stream with
+--       startPos := p1
+--       stopPos := p2
+--     }
 
 def Parser.ws : Parser Unit := do
   Parser.dropMany <| Parser.tokenFilter <| Char.isWhitespace
diff --git a/Http/URI.lean b/Http/URI.lean
index d89c7cc..68a49d5 100644
--- a/Http/URI.lean
+++ b/Http/URI.lean
@@ -100,7 +100,7 @@ structure URI where
   fragment : Option Fragment
 deriving Inhabited
 
-end Http open Parser
+end Http open Parser Char
 namespace Http
 
 open Http.Parser
@@ -136,28 +136,28 @@ URLs.
 -/
 
 def Scheme.parse : Parser Scheme := do
-  let str ← capture <| do
+  let str ← captureString <| do
     let _ ← tokenFilter (·.isAlpha)
     let _ ← dropMany <| tokenFilter (fun c => c.isAlphanum || c ∈ ['+', '-', '.'])
-  return Scheme.ofString str.toString |>.get!
+  return Scheme.ofString str.2.toString |>.get!
 
 def Authority.UserInfo.parse : Parser Authority.UserInfo := do
-  let user : Substring ←
-    capture <| dropMany <| tokenFilter (·.isAlphanum)
-  let pword : Option Substring ←
-    withBacktracking (token ':' *> some <$> (capture <| dropMany <| tokenFilter (·.isAlphanum)))
+  let user ←
+    captureString <| dropMany <| tokenFilter (·.isAlphanum)
+  let pword : Option (Unit × Substring) ←
+    withBacktracking (token ':' *> some <$> (captureString <| dropMany <| tokenFilter (·.isAlphanum)))
     <|> pure none
   let _ ← token '@'
-  return ⟨user.toString, pword.map (·.toString)⟩
+  return ⟨user.2.toString, pword.map (·.2.toString)⟩
 
 def Authority.Hostname.parse : Parser Authority.Hostname := do
-  let str ← capture <| dropMany <| tokenFilter (fun c => c.isAlphanum || c = '-' || c = '.')
-  return str.toString
+  let str ← captureString <| dropMany <| tokenFilter (fun c => c.isAlphanum || c = '-' || c = '.')
+  return str.2.toString
 
 def Authority.Port.parse : Parser Authority.Port := do
   let _ ← token ':'
-  let digs ← capture <| dropMany <| tokenFilter (·.isDigit)
-  match digs.toString.toNat? with
+  let digs ← captureString <| dropMany <| tokenFilter (·.isDigit)
+  match digs.2.toString.toNat? with
   | none =>
     throwUnexpectedWithMessage none s!"BUG: captured non-digit??: {digs}"
   | some num =>
@@ -197,7 +197,7 @@ def Path.pctEnc : Parser Char := do
 
 def Path.parse : Parser Path := do
   let parts ← takeMany <|
-    token '/' *> (capture <| dropMany <|
+    token '/' *> (captureString <| dropMany <|
       (tokenFilter (fun c =>
         if h : c.toNat < 256 then
           Path.allowedSegChars[c.toNat]'(Path.allowedSegChars_size ▸ h) > 0
@@ -207,17 +207,17 @@ def Path.parse : Parser Path := do
       <|>
       Path.pctEnc)
     )
-  return parts.map (·.toString)
+  return parts.map (·.2.toString)
 
 def Query.parse : Parser Query := do
   let _ ← token '?'
-  let str ← capture <| dropMany <| tokenFilter (fun c => c != '#')
-  return str.toString
+  let str ← captureString <| dropMany <| tokenFilter (fun c => c != '#')
+  return str.2.toString
 
 def Fragment.parse : Parser Fragment := do
   let _ ← token '#'
-  let str ← capture <| dropMany anyToken
-  return str.toString
+  let str ← captureString <| dropMany anyToken
+  return str.2.toString
 
 def parse : Parser URI := do
   let scheme ← option? <| withBacktracking do
diff --git a/lake-manifest.json b/lake-manifest.json
index 85e899d..6376a16 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -31,7 +31,7 @@
   {"url": "https://github.com/fgdorais/lean4-parser",
    "type": "git",
    "subDir": null,
-   "rev": "9af869c770afa8572e0c4854b0a3dd33c48ea735",
+   "rev": "bb2fe27511eecfb25f50d45171dfdecd6d7a82e2",
    "name": "Parser",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

From cf6178a5948a698c36e05ffc82c439844d66538e Mon Sep 17 00:00:00 2001
From: James <jamesgallicchio@gmail.com>
Date: Fri, 22 Dec 2023 12:52:23 -0500
Subject: [PATCH 3/6] Add CI

---
 .github/workflows/build.yml | 22 ++++++++++++++++++++++
 .gitignore                  |  4 ++--
 2 files changed, 24 insertions(+), 2 deletions(-)
 create mode 100644 .github/workflows/build.yml

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
new file mode 100644
index 0000000..628d858
--- /dev/null
+++ b/.github/workflows/build.yml
@@ -0,0 +1,22 @@
+on:
+  push:
+  pull_request:
+
+name: ci
+
+jobs:
+  build:
+    name: Build
+    runs-on: ubuntu-latest
+    steps:
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - uses: actions/checkout@v2
+
+      - name: build package
+        run: lake exe cache get && lake build
diff --git a/.gitignore b/.gitignore
index 0329f0b..e7b772d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,4 @@
 *.olean
-result*
+lake-packages
 lean_packages
-build
\ No newline at end of file
+build

From ec2b0a2a2423fd87b25907055bf36e058b4c7333 Mon Sep 17 00:00:00 2001
From: James <jamesgallicchio@gmail.com>
Date: Fri, 22 Dec 2023 12:55:44 -0500
Subject: [PATCH 4/6] fix: no mathlib cache :)

---
 .github/workflows/build.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 628d858..2dc6762 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -19,4 +19,4 @@ jobs:
       - uses: actions/checkout@v2
 
       - name: build package
-        run: lake exe cache get && lake build
+        run: lake build

From 077c8aa330d7162fe66ee05849f75d7b56c3d706 Mon Sep 17 00:00:00 2001
From: James Gallicchio <JamesGallicchio@users.noreply.github.com>
Date: Fri, 22 Dec 2023 12:54:06 -0500
Subject: [PATCH 5/6] chore: cleanup old eval

---
 Http/URI.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Http/URI.lean b/Http/URI.lean
index 68a49d5..8a16411 100644
--- a/Http/URI.lean
+++ b/Http/URI.lean
@@ -235,5 +235,3 @@ def fromString? (s : String) : Option URI :=
   | .ok ss u =>
     if ss.isEmpty then some u else none
   | _ => none
-
--- #eval fromString? "https://api.github.com" |>.map (·.appendPath #["hi"])

From 250473509a1500e6e2386e63cec7e2e503be3814 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Sat, 23 Dec 2023 01:09:49 -0500
Subject: [PATCH 6/6] fix: new capture functions

---
 Http/HeaderName.lean |  2 +-
 Http/Headers.lean    |  2 +-
 Http/URI.lean        | 16 ++++++++--------
 lake-manifest.json   |  4 ++--
 4 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/Http/HeaderName.lean b/Http/HeaderName.lean
index 2f31a8e..868e423 100644
--- a/Http/HeaderName.lean
+++ b/Http/HeaderName.lean
@@ -921,6 +921,6 @@ end Http.HeaderName open Parser Char open Http.Parser
 namespace Http.HeaderName
 
 def parse : Parser HeaderName := do
-  let str ← captureString <| dropMany1 (tokenFilter (fun c => Char.isAlphanum c ||
+  let str ← captureStr <| dropMany1 (tokenFilter (fun c => Char.isAlphanum c ||
             c ∈ ['-', '_', '!', '#', '$', '%', '&', '|', '*', '+', '.', '^', '"', '\'', '`']))
   return HeaderName.ofHeaderString str.2.toString
diff --git a/Http/Headers.lean b/Http/Headers.lean
index 11f3091..1111800 100644
--- a/Http/Headers.lean
+++ b/Http/Headers.lean
@@ -42,7 +42,7 @@ def parseHeader : Parser (HeaderName × String) := do
   ws
   let _ ← Parser.token ':'
   ws
-  let value ← captureString <| Parser.dropMany <| Parser.tokenFilter (fun c => c != '\n')
+  let value ← captureStr <| Parser.dropMany <| Parser.tokenFilter (fun c => c != '\n')
   ws
   return (key, value.2.toString)
 
diff --git a/Http/URI.lean b/Http/URI.lean
index 8a16411..bce8d6c 100644
--- a/Http/URI.lean
+++ b/Http/URI.lean
@@ -136,27 +136,27 @@ URLs.
 -/
 
 def Scheme.parse : Parser Scheme := do
-  let str ← captureString <| do
+  let str ← captureStr <| do
     let _ ← tokenFilter (·.isAlpha)
     let _ ← dropMany <| tokenFilter (fun c => c.isAlphanum || c ∈ ['+', '-', '.'])
   return Scheme.ofString str.2.toString |>.get!
 
 def Authority.UserInfo.parse : Parser Authority.UserInfo := do
   let user ←
-    captureString <| dropMany <| tokenFilter (·.isAlphanum)
+    captureStr <| dropMany <| tokenFilter (·.isAlphanum)
   let pword : Option (Unit × Substring) ←
-    withBacktracking (token ':' *> some <$> (captureString <| dropMany <| tokenFilter (·.isAlphanum)))
+    withBacktracking (token ':' *> some <$> (captureStr <| dropMany <| tokenFilter (·.isAlphanum)))
     <|> pure none
   let _ ← token '@'
   return ⟨user.2.toString, pword.map (·.2.toString)⟩
 
 def Authority.Hostname.parse : Parser Authority.Hostname := do
-  let str ← captureString <| dropMany <| tokenFilter (fun c => c.isAlphanum || c = '-' || c = '.')
+  let str ← captureStr <| dropMany <| tokenFilter (fun c => c.isAlphanum || c = '-' || c = '.')
   return str.2.toString
 
 def Authority.Port.parse : Parser Authority.Port := do
   let _ ← token ':'
-  let digs ← captureString <| dropMany <| tokenFilter (·.isDigit)
+  let digs ← captureStr <| dropMany <| tokenFilter (·.isDigit)
   match digs.2.toString.toNat? with
   | none =>
     throwUnexpectedWithMessage none s!"BUG: captured non-digit??: {digs}"
@@ -197,7 +197,7 @@ def Path.pctEnc : Parser Char := do
 
 def Path.parse : Parser Path := do
   let parts ← takeMany <|
-    token '/' *> (captureString <| dropMany <|
+    token '/' *> (captureStr <| dropMany <|
       (tokenFilter (fun c =>
         if h : c.toNat < 256 then
           Path.allowedSegChars[c.toNat]'(Path.allowedSegChars_size ▸ h) > 0
@@ -211,12 +211,12 @@ def Path.parse : Parser Path := do
 
 def Query.parse : Parser Query := do
   let _ ← token '?'
-  let str ← captureString <| dropMany <| tokenFilter (fun c => c != '#')
+  let str ← captureStr <| dropMany <| tokenFilter (fun c => c != '#')
   return str.2.toString
 
 def Fragment.parse : Parser Fragment := do
   let _ ← token '#'
-  let str ← captureString <| dropMany anyToken
+  let str ← captureStr <| dropMany anyToken
   return str.2.toString
 
 def parse : Parser URI := do
diff --git a/lake-manifest.json b/lake-manifest.json
index 6376a16..aba425c 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "ee49cf8fada1bf5a15592c399a925c401848227f",
+   "rev": "7d065f253ed92e9c3b45751cdfc52bc1e9507561",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -31,7 +31,7 @@
   {"url": "https://github.com/fgdorais/lean4-parser",
    "type": "git",
    "subDir": null,
-   "rev": "bb2fe27511eecfb25f50d45171dfdecd6d7a82e2",
+   "rev": "df99295b089c215baa7b2c5d5ef5359ba3283115",
    "name": "Parser",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",