Skip to content

Commit

Permalink
Merge pull request #54 from objectionary/update-toolchain
Browse files Browse the repository at this point in the history 
Update lean toolchain
  • Loading branch information
@eyihluyc
eyihluyc authored Dec 6, 2024
2 parents 8d5729a + cb0175b commit fa4f453
Show file tree
Hide file tree
Showing 2 changed files with 66 additions and 56 deletions.
120 changes: 65 additions & 55 deletions lake-manifest.json
View file
Original file line number Diff line number Diff line change
@@ -1,125 +1,135 @@
{"version": "1.1.0",
"packagesDir": ".lake/packages",
"packages":
[{"url": "https://github.com/acmepjz/md4lean",
[{"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"scope": "",
"rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
"name": "MD4Lean",
"rev": "c016aa9938c4cedc9b7066099f99bcae1b1af625",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
"inherited": false,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "7afce91e4fcee25c1ed06dca8d71b82bed396776",
"name": "UnicodeBasic",
"rev": "e80c9183755c1371c29bd4f5af338f77b8ac2851",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"inputRev": null,
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/dupuisf/BibtexQuery",
{"url": "https://github.com/leanprover/doc-gen4",
"type": "git",
"subDir": null,
"scope": "",
"rev": "0a294fe9bf23b396c5cc955054c50b9b652ec5ad",
"name": "BibtexQuery",
"rev": "099b90e374ba73983c3fda87595be625f1931669",
"name": "«doc-gen4»",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": true,
"inputRev": "main",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/mhuisi/lean4-cli",
{"url": "https://github.com/leanprover-community/plausible",
"type": "git",
"subDir": null,
"scope": "",
"rev": "bf066c328bcff19aa93adf4d24c4e896c0d4eaca",
"name": "Cli",
"scope": "leanprover-community",
"rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35",
"name": "plausible",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly",
"inputRev": "v4.15.0-rc1",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover/doc-gen4",
{"url": "https://github.com/leanprover-community/LeanSearchClient",
"type": "git",
"subDir": null,
"scope": "",
"rev": "1b0072fea2aa6a0ef8ef8b506ec5223b184cb4d0",
"name": "«doc-gen4»",
"scope": "leanprover-community",
"rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
"name": "LeanSearchClient",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/batteries",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/import-graph",
"type": "git",
"subDir": null,
"scope": "",
"rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
"name": "batteries",
"scope": "leanprover-community",
"rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/quote4",
"inputRev": "v4.15.0-rc1",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/ProofWidgets4",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
"name": "Qq",
"rev": "2b000e02d50394af68cfb4770a291113d94801b5",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inputRev": "v0.0.48",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "662f986ad3c5ad6ab1a1726b3c04f5ec425aa9f7",
"rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/ProofWidgets4",
{"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
"name": "proofwidgets",
"rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "v0.0.42",
"inputRev": "v4.14.0",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/import-graph",
{"url": "https://github.com/leanprover/lean4-cli",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
"name": "importGraph",
"scope": "leanprover",
"rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/siddhartha-gadgil/LeanSearchClient.git",
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
"type": "git",
"subDir": null,
"scope": "",
"rev": "c260ed920e2ebd23ef9fc8ca3fd24115e04c18b1",
"name": "LeanSearchClient",
"rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff",
"name": "UnicodeBasic",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/mathlib4.git",
"configFile": "lakefile.lean"},
{"url": "https://github.com/dupuisf/BibtexQuery",
"type": "git",
"subDir": null,
"scope": "",
"rev": "7eb3f52a4fc12036cb1c4a953dd0f497b57a2434",
"name": "mathlib",
"rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b",
"name": "BibtexQuery",
"manifestFile": "lake-manifest.json",
"inputRev": null,
"inherited": false,
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/acmepjz/md4lean",
"type": "git",
"subDir": null,
"scope": "",
"rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c",
"name": "MD4Lean",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"}],
"name": "«phi-calculus»",
"lakeDir": ".lake"}
2 changes: 1 addition & 1 deletion lean-toolchain
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.12.0-rc1
leanprover/lean4:v4.15.0-rc1

1 comment on commit fa4f453

@0pdd
Copy link

@0pdd 0pdd commented on fa4f453 Dec 6, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wasn't able to retrieve PDD puzzles from the code base and submit them to github. If you think that it's a bug on our side, please submit it to yegor256/0pdd:

set -x && set -e && set -o pipefail && cd /tmp/0pdd20241206-2-aqllo6/Z2l0QGdpdGh1Yi5jb206b2JqZWN0aW9uYXJ5L3Byb29mLmdpdA && pdd -v -f /tmp/20241206-3508-lwo8yj [1]: + set -e + set -o pipefail + cd /tmp/0pdd20241206-2-aqllo6/Z2l0QGdpdGh1Yi5jb206b2JqZWN0aW9uYXJ5L3Byb29mLmdpdA + pdd -v -f...

Please, copy and paste this stack trace to GitHub:

UserError
set -x && set -e && set -o pipefail && cd /tmp/0pdd20241206-2-aqllo6/Z2l0QGdpdGh1Yi5jb206b2JqZWN0aW9uYXJ5L3Byb29mLmdpdA && pdd -v -f /tmp/20241206-3508-lwo8yj [1]:
+ set -e
+ set -o pipefail
+ cd /tmp/0pdd20241206-2-aqllo6/Z2l0QGdpdGh1Yi5jb206b2JqZWN0aW9uYXJ5L3Byb29mLmdpdA
+ pdd -v -f /tmp/20241206-3508-lwo8yj

My version is 0.24.0
Ruby version is 3.1.4 at x86_64-linux
Reading from root dir /tmp/0pdd20241206-2-aqllo6/Z2l0QGdpdGh1Yi5jb206b2JqZWN0aW9uYXJ5L3Byb29mLmdpdA
/tmp/0pdd20241206-2-aqllo6/Z2l0QGdpdGh1Yi5jb206b2JqZWN0aW9uYXJ5L3Byb29mLmdpdA/lake-manifest.json is a binary file (4329 bytes)
/tmp/0pdd20241206-2-aqllo6/Z2l0QGdpdGh1Yi5jb206b2JqZWN0aW9uYXJ5L3Byb29mLmdpdA/renovate.json is a binary file (114 bytes)
Reading .github/workflows/lean.yml ...
Reading .gitignore ...
Reading Extended/ARS.lean ...
Reading Extended/Confluence/CompleteDevelopment.lean ...
Reading Extended/Confluence/Equivalence.lean ...
Reading Extended/Record.lean ...
Reading Extended/Reduction/Parallel/Definition.lean ...
Reading Extended/Reduction/Parallel/Properties.lean ...
Reading Extended/Reduction/Regular/Definition.lean ...
ERROR: ERROR: Extended/Reduction/Regular/Definition.lean; PDD::Error at Extended/Reduction/Regular/Definition.lean:102: TODO found, but puzzle can't be parsed, most probably because TODO is not followed by a puzzle marker, as this page explains: https://github.com/cqfn/pdd#how-to-format
If you can't understand the cause of this issue or you don't know how to fix it, please submit a GitHub issue, we will try to help you: https://github.com/cqfn/pdd/issues. This tool is still in its beta version and we will appreciate your feedback. Here is where you can find more documentation: https://github.com/cqfn/pdd/blob/master/README.md.
Exit code is 1

/app/objects/git_repo.rb:74:in `rescue in block in xml'
/app/objects/git_repo.rb:71:in `block in xml'
/app/vendor/ruby-3.1.4/lib/ruby/3.1.0/tempfile.rb:317:in `open'
/app/objects/git_repo.rb:70:in `xml'
/app/objects/puzzles.rb:46:in `deploy'
/app/objects/jobs/job.rb:38:in `proceed'
/app/objects/jobs/job_starred.rb:32:in `proceed'
/app/objects/jobs/job_recorded.rb:31:in `proceed'
/app/objects/jobs/job_emailed.rb:33:in `proceed'
/app/objects/jobs/job_commiterrors.rb:33:in `proceed'
/app/objects/jobs/job_detached.rb:48:in `exclusive'
/app/objects/jobs/job_detached.rb:36:in `block in proceed'
/app/objects/jobs/job_detached.rb:36:in `fork'
/app/objects/jobs/job_detached.rb:36:in `proceed'
/app/0pdd.rb:549:in `process_request'
/app/0pdd.rb:380:in `block in <top (required)>'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1804:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1804:in `block in compile!'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1071:in `block (3 levels) in route!'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1089:in `route_eval'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1071:in `block (2 levels) in route!'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1120:in `block in process_route'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1118:in `catch'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1118:in `process_route'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1069:in `block in route!'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1066:in `each'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1066:in `route!'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1190:in `block in dispatch!'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1161:in `catch'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1161:in `invoke'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1185:in `dispatch!'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1001:in `block in call!'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1161:in `catch'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1161:in `invoke'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1001:in `call!'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:990:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/rack-3.0.9/lib/rack/rewindable_input.rb:25:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/rack-3.0.9/lib/rack/deflater.rb:47:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/rack-protection-4.0.0/lib/rack/protection/xss_header.rb:20:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/rack-protection-4.0.0/lib/rack/protection/path_traversal.rb:18:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/rack-protection-4.0.0/lib/rack/protection/json_csrf.rb:28:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/rack-protection-4.0.0/lib/rack/protection/base.rb:53:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/rack-protection-4.0.0/lib/rack/protection/base.rb:53:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/rack-protection-4.0.0/lib/rack/protection/frame_options.rb:33:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/rack-3.0.9/lib/rack/logger.rb:19:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/rack-3.0.9/lib/rack/common_logger.rb:43:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:266:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:259:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/rack-3.0.9/lib/rack/head.rb:15:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/rack-3.0.9/lib/rack/method_override.rb:28:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:224:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:2115:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1674:in `block in call'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1890:in `synchronize'
/app/vendor/bundle/ruby/3.1.0/gems/sinatra-4.0.0/lib/sinatra/base.rb:1674:in `call'
/app/vendor/bundle/ruby/3.1.0/gems/rackup-2.1.0/lib/rackup/handler/webrick.rb:111:in `service'
/app/vendor/bundle/ruby/3.1.0/gems/webrick-1.8.1/lib/webrick/httpserver.rb:140:in `service'
/app/vendor/bundle/ruby/3.1.0/gems/webrick-1.8.1/lib/webrick/httpserver.rb:96:in `run'
/app/vendor/bundle/ruby/3.1.0/gems/webrick-1.8.1/lib/webrick/server.rb:310:in `block in start_thread'

Please sign in to comment.