Skip to content

[#15109] test toolchain: stricter check for dsimp lemmas - #68

Draft
downstream-lean4[bot] wants to merge 3 commits into
masterfrom
adaptation-15109
Draft

[#15109] test toolchain: stricter check for dsimp lemmas#68
downstream-lean4[bot] wants to merge 3 commits into
masterfrom
adaptation-15109

Conversation

@downstream-lean4

Copy link
Copy Markdown
Contributor

This is the adaptation PR for leanprover/lean4#15109.

@downstream-lean4

Copy link
Copy Markdown
Contributor Author

Build report for remove unnecessary options

Turned red:

Repo Critical Build Test Lint
batteries ✅ in 5s 🟥 in 4s ✅ in 2s
mathlib4 🟥 in 223s ⏭️ ⏭️
reference-manual 🟥 in 74s ⏭️ ⏭️
cslib ⏭️ ⏭️ ⏭️
repl ✅ in 1s 🟥 in 32s ⏭️
Stayed green
Repo Critical Build Test Lint
aesop ✅ in 7s ✅ in 5s ⏭️
import-graph ✅ in 2s ✅ in 4s ⏭️
lean4-cli ✅ in 1s ✅ in 0s ⏭️
plausible ✅ in 1s ✅ in 2s ⏭️
ProofWidgets4 ✅ in 3s ✅ in 1s ⏭️
quote4 ✅ in 2s ✅ in 1s ⏭️
BibtexQuery ✅ in 3s ⏭️ ⏭️
comparator ✅ in 2s ⏭️ ⏭️
doc-gen4 ✅ in 9s ⏭️ ⏭️
illuminate ✅ in 4s ✅ in 10s ⏭️
lean4-unicode-basic ✅ in 2s ⏭️ ⏭️
lean4export ✅ in 0s ✅ in 7s ⏭️
LeanSearchClient ✅ in 1s ✅ in 0s ⏭️
leansqlite ✅ in 7s ✅ in 15s ⏭️
nerodia ✅ in 2s ✅ in 21s ⏭️
verso ✅ in 91s ✅ in 84s ⏭️
verso-slides ✅ in 58s ✅ in 6s ⏭️
verso-web-components ✅ in 34s ⏭️ ⏭️

View run

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

adaptation This is an adaptation PR for a PR in the lean4 repository. cache-available toolchain-available

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant