Created
November 22, 2023 03:05
-
-
Save alreadydone/5299197dc88b8237a4896803ac9a915f to your computer and use it in GitHub Desktop.
Interesting `refine'` bug from CI run https://github.com/leanprover-community/mathlib4/actions/runs/6951956751/job/18914770581?pr=8556
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 2023-11-22T02:15:59.7794991Z error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/build/lib /home/lean/.elan/toolchains/leanprover--lean4---v4.3.0-rc2/bin/lean -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false ./././Mathlib/CategoryTheory/Sites/Grothendieck.lean -R ././. -o ./.lake/build/lib/Mathlib/CategoryTheory/Sites/Grothendieck.olean -i ./.lake/build/lib/Mathlib/CategoryTheory/Sites/Grothendieck.ilean -c ./.lake/build/ir/Mathlib/CategoryTheory/Sites/Grothendieck.c | |
| 2023-11-22T02:15:59.7802783Z error: stdout: | |
| 2023-11-22T02:15:59.7805141Z ##[error]./././Mathlib/CategoryTheory/Sites/Grothendieck.lean:309:66: error: application type mismatch | |
| 2023-11-22T02:15:59.7806652Z completeLatticeOfInf | |
| 2023-11-22T02:15:59.7806982Z (WithTop | |
| 2023-11-22T02:15:59.8263195Z (WithTop | |
| 2023-11-22T02:15:59.8263864Z (WithTop | |
| 2023-11-22T02:15:59.8264777Z (WithTop | |
| 2023-11-22T02:15:59.8265177Z (WithTop | |
| 2023-11-22T02:15:59.8265530Z (WithTop | |
| 2023-11-22T02:15:59.8265892Z (WithTop | |
| 2023-11-22T02:15:59.8504084Z (WithTop | |
| 2023-11-22T02:15:59.8505244Z (WithTop | |
| 2023-11-22T02:15:59.8505840Z (WithTop | |
| 2023-11-22T02:15:59.8506238Z (WithTop | |
| 2023-11-22T02:15:59.8506646Z (WithTop | |
| 2023-11-22T02:15:59.8507063Z (WithTop | |
| 2023-11-22T02:15:59.8507667Z (WithTop | |
| 2023-11-22T02:15:59.8508122Z (WithTop | |
| 2023-11-22T02:15:59.8508566Z (WithTop | |
| 2023-11-22T02:15:59.8509043Z (WithTop | |
| 2023-11-22T02:15:59.8509522Z (WithTop | |
| 2023-11-22T02:15:59.8509999Z (WithTop | |
| 2023-11-22T02:15:59.8510488Z (WithTop | |
| 2023-11-22T02:15:59.8511072Z (WithTop | |
| 2023-11-22T02:15:59.8511592Z (WithTop | |
| 2023-11-22T02:15:59.8512111Z (WithTop | |
| 2023-11-22T02:15:59.8512710Z (WithTop | |
| 2023-11-22T02:15:59.8513253Z (WithTop | |
| 2023-11-22T02:15:59.8513800Z (WithTop | |
| 2023-11-22T02:15:59.8514353Z (WithTop | |
| 2023-11-22T02:15:59.8514920Z (WithTop | |
| 2023-11-22T02:15:59.8515482Z (WithTop | |
| 2023-11-22T02:15:59.8516050Z (WithTop | |
| 2023-11-22T02:15:59.8516629Z (WithTop | |
| 2023-11-22T02:15:59.8517200Z (WithTop | |
| 2023-11-22T02:15:59.8517789Z (WithTop | |
| 2023-11-22T02:15:59.8518391Z (WithTop | |
| 2023-11-22T02:15:59.8518993Z (WithTop | |
| 2023-11-22T02:15:59.8519597Z (WithTop | |
| 2023-11-22T02:15:59.8520202Z (WithTop | |
| 2023-11-22T02:15:59.8520817Z (WithTop | |
| 2023-11-22T02:15:59.8521440Z (WithTop | |
| 2023-11-22T02:15:59.8522068Z (WithTop | |
| 2023-11-22T02:15:59.8522688Z (WithTop | |
| 2023-11-22T02:15:59.8523329Z (WithTop | |
| 2023-11-22T02:15:59.8523973Z (WithTop | |
| 2023-11-22T02:15:59.8524624Z (WithTop | |
| 2023-11-22T02:15:59.8525280Z (WithTop | |
| 2023-11-22T02:15:59.8525934Z (WithTop | |
| 2023-11-22T02:15:59.8526591Z (WithTop | |
| 2023-11-22T02:15:59.8527252Z (WithTop | |
| 2023-11-22T02:15:59.8527921Z (WithTop | |
| 2023-11-22T02:15:59.8528758Z (WithTop | |
| 2023-11-22T02:15:59.8529541Z (WithTop | |
| 2023-11-22T02:15:59.8530202Z (WithTop | |
| 2023-11-22T02:15:59.8530881Z (WithTop | |
| 2023-11-22T02:15:59.8531566Z (WithTop | |
| 2023-11-22T02:15:59.8532256Z (WithTop | |
| 2023-11-22T02:15:59.8532950Z (WithTop | |
| 2023-11-22T02:15:59.8533650Z (WithTop | |
| 2023-11-22T02:15:59.8534348Z (WithTop | |
| 2023-11-22T02:15:59.8535052Z (WithTop | |
| 2023-11-22T02:15:59.8535755Z (WithTop | |
| 2023-11-22T02:15:59.8536470Z (WithTop | |
| 2023-11-22T02:15:59.8537180Z (WithTop | |
| 2023-11-22T02:15:59.8537900Z (WithTop | |
| 2023-11-22T02:15:59.8538619Z (WithTop | |
| 2023-11-22T02:15:59.8539350Z (WithTop | |
| 2023-11-22T02:15:59.8540062Z (WithTop | |
| 2023-11-22T02:15:59.8540820Z (WithTop | |
| 2023-11-22T02:15:59.8541551Z (WithTop | |
| 2023-11-22T02:15:59.8542480Z (WithTop | |
| 2023-11-22T02:15:59.8543218Z (WithTop | |
| 2023-11-22T02:15:59.8543965Z (WithTop | |
| 2023-11-22T02:15:59.8544710Z (WithTop | |
| 2023-11-22T02:15:59.8545472Z (WithTop | |
| 2023-11-22T02:15:59.8546225Z (WithTop | |
| 2023-11-22T02:15:59.8547113Z (WithTop | |
| 2023-11-22T02:15:59.8547980Z (WithTop | |
| 2023-11-22T02:15:59.8548748Z (WithTop | |
| 2023-11-22T02:15:59.8549522Z (WithTop | |
| 2023-11-22T02:15:59.8550298Z (WithTop | |
| 2023-11-22T02:15:59.8551080Z (WithTop | |
| 2023-11-22T02:15:59.8551873Z (WithTop | |
| 2023-11-22T02:15:59.8552658Z (WithTop | |
| 2023-11-22T02:15:59.8553445Z (WithTop | |
| 2023-11-22T02:15:59.8554234Z (WithTop | |
| 2023-11-22T02:15:59.8555037Z (WithTop | |
| 2023-11-22T02:15:59.8555836Z (WithTop | |
| 2023-11-22T02:15:59.8556639Z (WithTop | |
| 2023-11-22T02:15:59.8557435Z (WithTop | |
| 2023-11-22T02:15:59.8558256Z (WithTop | |
| 2023-11-22T02:15:59.8559070Z (WithTop | |
| 2023-11-22T02:15:59.8559895Z (WithTop | |
| 2023-11-22T02:15:59.8560715Z (WithTop | |
| 2023-11-22T02:15:59.8561537Z (WithTop | |
| 2023-11-22T02:15:59.8562369Z (WithTop | |
| 2023-11-22T02:15:59.8563323Z (WithTop | |
| 2023-11-22T02:15:59.8564246Z (WithTop | |
| 2023-11-22T02:15:59.8565082Z (WithTop | |
| 2023-11-22T02:15:59.8565926Z (WithTop | |
| 2023-11-22T02:15:59.8566777Z (WithTop | |
| 2023-11-22T02:15:59.8567626Z (WithTop | |
| 2023-11-22T02:15:59.8568472Z (WithTop | |
| 2023-11-22T02:15:59.8569332Z (WithTop | |
| 2023-11-22T02:15:59.8570200Z (WithTop | |
| 2023-11-22T02:15:59.8571065Z (WithTop | |
| 2023-11-22T02:15:59.8572001Z (WithTop | |
| 2023-11-22T02:15:59.8572873Z (WithTop | |
| 2023-11-22T02:15:59.8573744Z (WithTop | |
| 2023-11-22T02:15:59.8574619Z (WithTop | |
| 2023-11-22T02:15:59.8575523Z (WithTop | |
| 2023-11-22T02:15:59.8576407Z (WithTop | |
| 2023-11-22T02:15:59.8577398Z (WithTop | |
| 2023-11-22T02:15:59.8578365Z (WithTop | |
| 2023-11-22T02:15:59.8579263Z (WithTop | |
| 2023-11-22T02:15:59.8580162Z (WithTop | |
| 2023-11-22T02:15:59.8581073Z (WithTop | |
| 2023-11-22T02:15:59.8582121Z (WithTop | |
| 2023-11-22T02:15:59.8583229Z (WithTop | |
| 2023-11-22T02:15:59.8584340Z (WithTop | |
| 2023-11-22T02:15:59.8585458Z (WithTop | |
| 2023-11-22T02:15:59.8586580Z (WithTop | |
| 2023-11-22T02:15:59.8587711Z (WithTop | |
| 2023-11-22T02:15:59.8588847Z (WithTop | |
| 2023-11-22T02:15:59.8589979Z (WithTop | |
| 2023-11-22T02:15:59.8591124Z (WithTop | |
| 2023-11-22T02:15:59.8592274Z (WithTop | |
| 2023-11-22T02:15:59.8593621Z (WithTop | |
| 2023-11-22T02:15:59.8594941Z (WithTop | |
| 2023-11-22T02:15:59.8596392Z Ordinal.{?u.65542}))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | |
| 2023-11-22T02:15:59.8597287Z _ | |
| 2023-11-22T02:15:59.8597606Z argument | |
| 2023-11-22T02:15:59.8597940Z isGLB_sInf | |
| 2023-11-22T02:15:59.8598292Z has type | |
| 2023-11-22T02:15:59.8784339Z ∀ (s : Set (GrothendieckTopology ?m.69655)), IsGLB s (sInf s) : Prop | |
| 2023-11-22T02:15:59.8785244Z but is expected to have type | |
| 2023-11-22T02:15:59.8785798Z ∀ | |
| 2023-11-22T02:15:59.8786071Z (s : | |
| 2023-11-22T02:15:59.8786357Z Set | |
| 2023-11-22T02:15:59.8786655Z (WithTop | |
| 2023-11-22T02:15:59.8786974Z (WithTop | |
| 2023-11-22T02:15:59.8787279Z (WithTop | |
| 2023-11-22T02:15:59.8787728Z (WithTop | |
| 2023-11-22T02:15:59.8788076Z (WithTop | |
| 2023-11-22T02:15:59.8788429Z (WithTop | |
| 2023-11-22T02:15:59.8788793Z (WithTop | |
| 2023-11-22T02:15:59.8789167Z (WithTop | |
| 2023-11-22T02:15:59.8789549Z (WithTop | |
| 2023-11-22T02:15:59.8789930Z (WithTop | |
| 2023-11-22T02:15:59.8790336Z (WithTop | |
| 2023-11-22T02:15:59.8790760Z (WithTop | |
| 2023-11-22T02:15:59.8791221Z (WithTop | |
| 2023-11-22T02:15:59.8791668Z (WithTop | |
| 2023-11-22T02:15:59.8792145Z (WithTop | |
| 2023-11-22T02:15:59.8792623Z (WithTop | |
| 2023-11-22T02:15:59.8793090Z (WithTop | |
| 2023-11-22T02:15:59.8793582Z (WithTop | |
| 2023-11-22T02:15:59.8794093Z (WithTop | |
| 2023-11-22T02:15:59.8794611Z (WithTop | |
| 2023-11-22T02:15:59.8795142Z (WithTop | |
| 2023-11-22T02:15:59.8795672Z (WithTop | |
| 2023-11-22T02:15:59.8796215Z (WithTop | |
| 2023-11-22T02:15:59.8796756Z (WithTop | |
| 2023-11-22T02:15:59.8797292Z (WithTop | |
| 2023-11-22T02:15:59.8797850Z (WithTop | |
| 2023-11-22T02:15:59.8798424Z (WithTop | |
| 2023-11-22T02:15:59.8798997Z (WithTop | |
| 2023-11-22T02:15:59.8799574Z (WithTop | |
| 2023-11-22T02:15:59.8800150Z (WithTop | |
| 2023-11-22T02:15:59.8800741Z (WithTop | |
| 2023-11-22T02:15:59.8801333Z (WithTop | |
| 2023-11-22T02:15:59.8801928Z (WithTop | |
| 2023-11-22T02:15:59.8802515Z (WithTop | |
| 2023-11-22T02:15:59.8803529Z (WithTop | |
| 2023-11-22T02:15:59.8804148Z (WithTop | |
| 2023-11-22T02:15:59.8805047Z (WithTop | |
| 2023-11-22T02:15:59.8805673Z (WithTop | |
| 2023-11-22T02:15:59.8806314Z (WithTop | |
| 2023-11-22T02:15:59.8806957Z (WithTop | |
| 2023-11-22T02:15:59.8807607Z (WithTop | |
| 2023-11-22T02:15:59.8808414Z (WithTop | |
| 2023-11-22T02:15:59.8809073Z (WithTop | |
| 2023-11-22T02:15:59.8809722Z (WithTop | |
| 2023-11-22T02:15:59.8810384Z (WithTop | |
| 2023-11-22T02:15:59.8811037Z (WithTop | |
| 2023-11-22T02:15:59.8811706Z (WithTop | |
| 2023-11-22T02:15:59.8812464Z (WithTop | |
| 2023-11-22T02:15:59.8813135Z (WithTop | |
| 2023-11-22T02:15:59.8813808Z (WithTop | |
| 2023-11-22T02:15:59.8814490Z (WithTop | |
| 2023-11-22T02:15:59.8815184Z (WithTop | |
| 2023-11-22T02:15:59.8815870Z (WithTop | |
| 2023-11-22T02:15:59.8816557Z (WithTop | |
| 2023-11-22T02:15:59.8817260Z (WithTop | |
| 2023-11-22T02:15:59.8817947Z (WithTop | |
| 2023-11-22T02:15:59.8818647Z (WithTop | |
| 2023-11-22T02:15:59.8819353Z (WithTop | |
| 2023-11-22T02:15:59.8820223Z (WithTop | |
| 2023-11-22T02:15:59.8820936Z (WithTop | |
| 2023-11-22T02:15:59.8821655Z (WithTop | |
| 2023-11-22T02:15:59.8822487Z (WithTop | |
| 2023-11-22T02:15:59.8823215Z (WithTop | |
| 2023-11-22T02:15:59.8824101Z (WithTop | |
| 2023-11-22T02:15:59.8824981Z (WithTop | |
| 2023-11-22T02:15:59.8825715Z (WithTop | |
| 2023-11-22T02:15:59.8826466Z (WithTop | |
| 2023-11-22T02:15:59.8827201Z (WithTop | |
| 2023-11-22T02:15:59.8827940Z (WithTop | |
| 2023-11-22T02:15:59.8828685Z (WithTop | |
| 2023-11-22T02:15:59.8829444Z (WithTop | |
| 2023-11-22T02:15:59.8830192Z (WithTop | |
| 2023-11-22T02:15:59.8830946Z (WithTop | |
| 2023-11-22T02:15:59.8831705Z (WithTop | |
| 2023-11-22T02:15:59.8832463Z (WithTop | |
| 2023-11-22T02:15:59.8833229Z (WithTop | |
| 2023-11-22T02:15:59.8834000Z (WithTop | |
| 2023-11-22T02:15:59.8834767Z (WithTop | |
| 2023-11-22T02:15:59.8835544Z (WithTop | |
| 2023-11-22T02:15:59.8836328Z (WithTop | |
| 2023-11-22T02:15:59.8837111Z (WithTop | |
| 2023-11-22T02:15:59.8837892Z (WithTop | |
| 2023-11-22T02:15:59.8838681Z (WithTop | |
| 2023-11-22T02:15:59.8839475Z (WithTop | |
| 2023-11-22T02:15:59.8840385Z (WithTop | |
| 2023-11-22T02:15:59.8841275Z (WithTop | |
| 2023-11-22T02:15:59.8842161Z (WithTop | |
| 2023-11-22T02:15:59.8842972Z (WithTop | |
| 2023-11-22T02:15:59.8843784Z (WithTop | |
| 2023-11-22T02:15:59.8844601Z (WithTop | |
| 2023-11-22T02:15:59.8845419Z (WithTop | |
| 2023-11-22T02:15:59.8846245Z (WithTop | |
| 2023-11-22T02:15:59.8847071Z (WithTop | |
| 2023-11-22T02:15:59.8847900Z (WithTop | |
| 2023-11-22T02:15:59.8848733Z (WithTop | |
| 2023-11-22T02:15:59.8849566Z (WithTop | |
| 2023-11-22T02:15:59.8850403Z (WithTop | |
| 2023-11-22T02:15:59.8851238Z (WithTop | |
| 2023-11-22T02:15:59.8852081Z (WithTop | |
| 2023-11-22T02:15:59.8852934Z (WithTop | |
| 2023-11-22T02:15:59.8853783Z (WithTop | |
| 2023-11-22T02:15:59.8854634Z (WithTop | |
| 2023-11-22T02:15:59.8855606Z (WithTop | |
| 2023-11-22T02:15:59.8856568Z (WithTop | |
| 2023-11-22T02:15:59.8857432Z (WithTop | |
| 2023-11-22T02:15:59.8858300Z (WithTop | |
| 2023-11-22T02:15:59.8859203Z (WithTop | |
| 2023-11-22T02:15:59.8860089Z (WithTop | |
| 2023-11-22T02:15:59.8860966Z (WithTop | |
| 2023-11-22T02:15:59.8861933Z (WithTop | |
| 2023-11-22T02:15:59.8862828Z (WithTop | |
| 2023-11-22T02:15:59.8863730Z (WithTop | |
| 2023-11-22T02:15:59.8864624Z (WithTop | |
| 2023-11-22T02:15:59.8865517Z (WithTop | |
| 2023-11-22T02:15:59.8866419Z (WithTop | |
| 2023-11-22T02:15:59.8867330Z (WithTop | |
| 2023-11-22T02:15:59.8868237Z (WithTop | |
| 2023-11-22T02:15:59.8869266Z (WithTop | |
| 2023-11-22T02:15:59.8870287Z (WithTop | |
| 2023-11-22T02:15:59.8871208Z (WithTop | |
| 2023-11-22T02:15:59.8872192Z (WithTop | |
| 2023-11-22T02:15:59.8873119Z (WithTop | |
| 2023-11-22T02:15:59.8874057Z (WithTop | |
| 2023-11-22T02:15:59.8874993Z (WithTop | |
| 2023-11-22T02:15:59.8875927Z (WithTop | |
| 2023-11-22T02:15:59.8876862Z (WithTop | |
| 2023-11-22T02:15:59.8877806Z (WithTop | |
| 2023-11-22T02:15:59.8878995Z Ordinal.{?u.65542})))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), | |
| 2023-11-22T02:15:59.8879773Z IsGLB s (sInf s) : Prop | |
| 2023-11-22T02:15:59.8881408Z ##[error]./././Mathlib/CategoryTheory/Sites/Grothendieck.lean:309:43: error: failed to synthesize | |
| 2023-11-22T02:15:59.8882812Z InfSet | |
| 2023-11-22T02:15:59.8883084Z (WithTop | |
| 2023-11-22T02:15:59.8883373Z (WithTop | |
| 2023-11-22T02:15:59.8883676Z (WithTop | |
| 2023-11-22T02:15:59.8883984Z (WithTop | |
| 2023-11-22T02:15:59.8884290Z (WithTop | |
| 2023-11-22T02:15:59.8884612Z (WithTop | |
| 2023-11-22T02:15:59.8884944Z (WithTop | |
| 2023-11-22T02:15:59.8885275Z (WithTop | |
| 2023-11-22T02:15:59.8885631Z (WithTop | |
| 2023-11-22T02:15:59.8885998Z (WithTop | |
| 2023-11-22T02:15:59.8886372Z (WithTop | |
| 2023-11-22T02:15:59.8886758Z (WithTop | |
| 2023-11-22T02:15:59.8887161Z (WithTop | |
| 2023-11-22T02:15:59.8887751Z (WithTop | |
| 2023-11-22T02:15:59.8888176Z (WithTop | |
| 2023-11-22T02:15:59.8888761Z (WithTop | |
| 2023-11-22T02:15:59.8889226Z (WithTop | |
| 2023-11-22T02:15:59.8889701Z (WithTop | |
| 2023-11-22T02:15:59.8890176Z (WithTop | |
| 2023-11-22T02:15:59.8890661Z (WithTop | |
| 2023-11-22T02:15:59.8891166Z (WithTop | |
| 2023-11-22T02:15:59.8891675Z (WithTop | |
| 2023-11-22T02:15:59.8892181Z (WithTop | |
| 2023-11-22T02:15:59.8892704Z (WithTop | |
| 2023-11-22T02:15:59.8893246Z (WithTop | |
| 2023-11-22T02:15:59.8893783Z (WithTop | |
| 2023-11-22T02:15:59.8894334Z (WithTop | |
| 2023-11-22T02:15:59.8894889Z (WithTop | |
| 2023-11-22T02:15:59.8895450Z (WithTop | |
| 2023-11-22T02:15:59.8896010Z (WithTop | |
| 2023-11-22T02:15:59.8896565Z (WithTop | |
| 2023-11-22T02:15:59.8897135Z (WithTop | |
| 2023-11-22T02:15:59.8897717Z (WithTop | |
| 2023-11-22T02:15:59.8898301Z (WithTop | |
| 2023-11-22T02:15:59.8898886Z (WithTop | |
| 2023-11-22T02:15:59.8899476Z (WithTop | |
| 2023-11-22T02:15:59.8900080Z (WithTop | |
| 2023-11-22T02:15:59.8900862Z (WithTop | |
| 2023-11-22T02:15:59.8901481Z (WithTop | |
| 2023-11-22T02:15:59.8902302Z (WithTop | |
| 2023-11-22T02:15:59.8902935Z (WithTop | |
| 2023-11-22T02:15:59.8903571Z (WithTop | |
| 2023-11-22T02:15:59.8904202Z (WithTop | |
| 2023-11-22T02:15:59.8904836Z (WithTop | |
| 2023-11-22T02:15:59.8905488Z (WithTop | |
| 2023-11-22T02:15:59.8906145Z (WithTop | |
| 2023-11-22T02:15:59.8906780Z (WithTop | |
| 2023-11-22T02:15:59.8907436Z (WithTop | |
| 2023-11-22T02:15:59.8908101Z (WithTop | |
| 2023-11-22T02:15:59.8908761Z (WithTop | |
| 2023-11-22T02:15:59.8909429Z (WithTop | |
| 2023-11-22T02:15:59.8910095Z (WithTop | |
| 2023-11-22T02:15:59.8910955Z (WithTop | |
| 2023-11-22T02:15:59.8911758Z (WithTop | |
| 2023-11-22T02:15:59.8912441Z (WithTop | |
| 2023-11-22T02:15:59.8913128Z (WithTop | |
| 2023-11-22T02:15:59.8913823Z (WithTop | |
| 2023-11-22T02:15:59.8914517Z (WithTop | |
| 2023-11-22T02:15:59.8915207Z (WithTop | |
| 2023-11-22T02:15:59.8915910Z (WithTop | |
| 2023-11-22T02:15:59.8916620Z (WithTop | |
| 2023-11-22T02:15:59.8917330Z (WithTop | |
| 2023-11-22T02:15:59.8918037Z (WithTop | |
| 2023-11-22T02:15:59.8918749Z (WithTop | |
| 2023-11-22T02:15:59.8919467Z (WithTop | |
| 2023-11-22T02:15:59.8920194Z (WithTop | |
| 2023-11-22T02:15:59.8920922Z (WithTop | |
| 2023-11-22T02:15:59.8921637Z (WithTop | |
| 2023-11-22T02:15:59.8922370Z (WithTop | |
| 2023-11-22T02:15:59.8923107Z (WithTop | |
| 2023-11-22T02:15:59.8923844Z (WithTop | |
| 2023-11-22T02:15:59.8924587Z (WithTop | |
| 2023-11-22T02:15:59.8925337Z (WithTop | |
| 2023-11-22T02:15:59.8926083Z (WithTop | |
| 2023-11-22T02:15:59.8926818Z (WithTop | |
| 2023-11-22T02:15:59.8927569Z (WithTop | |
| 2023-11-22T02:15:59.8928434Z (WithTop | |
| 2023-11-22T02:15:59.8929282Z (WithTop | |
| 2023-11-22T02:15:59.8930055Z (WithTop | |
| 2023-11-22T02:15:59.8930831Z (WithTop | |
| 2023-11-22T02:15:59.8931613Z (WithTop | |
| 2023-11-22T02:15:59.8932475Z (WithTop | |
| 2023-11-22T02:15:59.8933265Z (WithTop | |
| 2023-11-22T02:15:59.8934054Z (WithTop | |
| 2023-11-22T02:15:59.8934850Z (WithTop | |
| 2023-11-22T02:15:59.8935641Z (WithTop | |
| 2023-11-22T02:15:59.8936447Z (WithTop | |
| 2023-11-22T02:15:59.8937251Z (WithTop | |
| 2023-11-22T02:15:59.8938053Z (WithTop | |
| 2023-11-22T02:15:59.8938859Z (WithTop | |
| 2023-11-22T02:15:59.8939669Z (WithTop | |
| 2023-11-22T02:15:59.8940507Z (WithTop | |
| 2023-11-22T02:15:59.8941618Z (WithTop | |
| 2023-11-22T02:15:59.9063623Z (WithTop | |
| 2023-11-22T02:15:59.9064589Z (WithTop | |
| 2023-11-22T02:15:59.9066183Z (WithTop | |
| 2023-11-22T02:15:59.9067323Z (WithTop | |
| 2023-11-22T02:15:59.9086825Z (WithTop | |
| 2023-11-22T02:15:59.9087715Z (WithTop | |
| 2023-11-22T02:15:59.9088588Z (WithTop | |
| 2023-11-22T02:15:59.9089446Z (WithTop | |
| 2023-11-22T02:15:59.9090313Z (WithTop | |
| 2023-11-22T02:15:59.9091168Z (WithTop | |
| 2023-11-22T02:15:59.9092121Z (WithTop | |
| 2023-11-22T02:15:59.9092994Z (WithTop | |
| 2023-11-22T02:15:59.9093875Z (WithTop | |
| 2023-11-22T02:15:59.9094746Z (WithTop | |
| 2023-11-22T02:15:59.9095617Z (WithTop | |
| 2023-11-22T02:15:59.9096509Z (WithTop | |
| 2023-11-22T02:15:59.9097402Z (WithTop | |
| 2023-11-22T02:15:59.9098285Z (WithTop | |
| 2023-11-22T02:15:59.9099164Z (WithTop | |
| 2023-11-22T02:15:59.9100447Z (WithTop | |
| 2023-11-22T02:15:59.9101523Z (WithTop | |
| 2023-11-22T02:15:59.9102543Z (WithTop | |
| 2023-11-22T02:15:59.9103459Z (WithTop | |
| 2023-11-22T02:15:59.9104364Z (WithTop | |
| 2023-11-22T02:15:59.9105262Z (WithTop | |
| 2023-11-22T02:15:59.9106159Z (WithTop | |
| 2023-11-22T02:15:59.9107066Z (WithTop | |
| 2023-11-22T02:15:59.9107989Z (WithTop | |
| 2023-11-22T02:15:59.9108909Z (WithTop | |
| 2023-11-22T02:15:59.9109826Z (WithTop | |
| 2023-11-22T02:15:59.9110756Z (WithTop | |
| 2023-11-22T02:15:59.9111692Z (WithTop | |
| 2023-11-22T02:15:59.9112628Z (WithTop | |
| 2023-11-22T02:15:59.9113677Z (WithTop | |
| 2023-11-22T02:15:59.9114960Z Ordinal.{?u.65542}))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | |
| 2023-11-22T02:15:59.9116782Z (deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) | |
| 2023-11-22T02:15:59.9119161Z ##[error]./././Mathlib/CategoryTheory/Sites/Grothendieck.lean:304:5: error: stuck at solving universe constraint | |
| 2023-11-22T02:15:59.9120688Z ?u.65542+1 =?= max u v | |
| 2023-11-22T02:15:59.9121056Z while trying to unify | |
| 2023-11-22T02:15:59.9123203Z @LE.le.{?u.65542 + 1} : {α : Type (?u.65542 + 1)} → [self : LE α] → α → α → Prop | |
| 2023-11-22T02:15:59.9123822Z with | |
| 2023-11-22T02:15:59.9124344Z @LE.le : {α : Type (max u v)} → [self : LE α] → α → α → Prop | |
| 2023-11-22T02:15:59.9125773Z ##[error]./././Mathlib/CategoryTheory/Sites/Grothendieck.lean:293:0: error: stuck at solving universe constraint | |
| 2023-11-22T02:15:59.9127228Z ?u.65542+1 =?= max u v | |
| 2023-11-22T02:15:59.9127594Z while trying to unify | |
| 2023-11-22T02:15:59.9128270Z @LE.le.{?u.65542 + 1} : {α : Type (?u.65542 + 1)} → [self : LE α] → α → α → Prop | |
| 2023-11-22T02:15:59.9128847Z with | |
| 2023-11-22T02:15:59.9129331Z @LE.le : {α : Type (max u v)} → [self : LE α] → α → α → Prop | |
| 2023-11-22T02:15:59.9130395Z ##[error]./././Mathlib/CategoryTheory/Sites/Grothendieck.lean:317:2: error: type mismatch | |
| 2023-11-22T02:15:59.9182800Z rfl | |
| 2023-11-22T02:15:59.9183118Z has type | |
| 2023-11-22T02:15:59.9183480Z trivial C = trivial C : Prop | |
| 2023-11-22T02:15:59.9183944Z but is expected to have type | |
| 2023-11-22T02:15:59.9184628Z trivial C = ⊥ : Prop | |
| 2023-11-22T02:15:59.9185949Z ##[error]./././Mathlib/CategoryTheory/Sites/Grothendieck.lean:322:2: error: type mismatch | |
| 2023-11-22T02:15:59.9187314Z rfl | |
| 2023-11-22T02:15:59.9187581Z has type | |
| 2023-11-22T02:15:59.9187912Z discrete C = discrete C : Prop | |
| 2023-11-22T02:15:59.9188365Z but is expected to have type | |
| 2023-11-22T02:15:59.9188838Z discrete C = ⊤ : Prop | |
| 2023-11-22T02:15:59.9189792Z ##[error]./././Mathlib/CategoryTheory/Sites/Grothendieck.lean:327:2: error: type mismatch | |
| 2023-11-22T02:15:59.9191140Z trivial_covering | |
| 2023-11-22T02:15:59.9191459Z has type | |
| 2023-11-22T02:15:59.9191899Z S ∈ sieves (trivial C) X ↔ S = ⊤ : Prop | |
| 2023-11-22T02:15:59.9192399Z but is expected to have type | |
| 2023-11-22T02:15:59.9192877Z S ∈ sieves ⊥ X ↔ S = ⊤ : Prop | |
| 2023-11-22T02:15:59.9194563Z ##[error]./././Mathlib/CategoryTheory/Sites/Grothendieck.lean:332:2: error: invalid constructor ⟨...⟩, expected type must be an inductive type | |
| 2023-11-22T02:15:59.9196228Z ⊤.1 X S | |
| 2023-11-22T02:15:59.9197168Z error: external command `/home/lean/.elan/toolchains/leanprover--lean4---v4.3.0-rc2/bin/lean` exited with code 1 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment