Error fetching results: CalledProcessError(1, 'lake env lean --threads 16 --run ExtractData.lean') #232
Unanswered
willejiang
asked this question in
Q&A
Replies: 1 comment 1 reply
-
|
same issue |
Beta Was this translation helpful? Give feedback.
1 reply
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Uh oh!
There was an error while loading. Please reload this page.
-
I am trying to run leanuniverse which will run leandojo in the process and I keep received the following log:
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '8cee626a680fe217814c4bd444b94ceb31efd6b6'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '8d29bc2c3ebe1f863c2f02df816b4f3dd1b65226'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'c20832d6f0b3186a97ea9361cec0a5b87dd152a3'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'ea953247aac573c9b5adea60bacd3e085f58aca4'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '57185dfad68d78356f9462af984882d6f262aa5d'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'aa4c87abed970d9dfad2506000d99d30b02f476b'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'f1a7afdb343196b33bf9137b232eb69446065925'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision 'aff4176e5c41737a0d73be74ad9feb6a889bfa98'
Build completed successfully.
0: INFO 25-04-09 00:30:08.437575 - 1:50:53 - [leanprover-community/mathlib4] Error fetching results: CalledProcessError(1, 'lake env lean --threads 16 --run ExtractData.lean')
100%|████████████████████████████████████████████████████████████████████████████████████████████| 1/1 [1:49:00<00:00, 6540.24s/it]
0: INFO 25-04-09 00:30:08.443695 - 1:50:53 - Saving database file to /home/jupyter/LeanUniverse/cache/database.json.
0: INFO 25-04-09 00:30:08.445606 - 1:50:53 - Report saved.
I wonder why there's a CalledProcessError and how to fix it?
Beta Was this translation helpful? Give feedback.
All reactions