-
Notifications
You must be signed in to change notification settings - Fork 0
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: add BitVec.toNat_[udiv|umod] and [udiv|umod]_eq #15
Commits on Aug 10, 2024
-
feat:
@[app_delab]
(leanprover#4976)Adds `@[app_delab ident]` as a macro for `@[delab app.ident]`. Resolves the identifier when expanding the macro, saving needing to use the fully qualified identifiers that `@[delab]` requires. Also, unlike `@[delab]`, throws an error if the identifier cannot be resolved. Closes leanprover#4899
Configuration menu - View commit details
-
Copy full SHA for 5f31e93 - Browse repository at this point
Copy the full SHA 5f31e93View commit details
Commits on Aug 11, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 4236d8a - Browse repository at this point
Copy the full SHA 4236d8aView commit details
Commits on Aug 12, 2024
-
fix: regular mvar assignments take precedence over delayed ones (lean…
…prover#4987) closes leanprover#4920
Configuration menu - View commit details
-
Copy full SHA for 2436562 - Browse repository at this point
Copy the full SHA 2436562View commit details -
Configuration menu - View commit details
-
Copy full SHA for 7d74475 - Browse repository at this point
Copy the full SHA 7d74475View commit details -
fix: omega regression (leanprover#4989)
This is a better fix to the problem reported at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nat.20fighting, which itself had a problem as reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/omega.20regression/near/456539091.
Configuration menu - View commit details
-
Copy full SHA for 215b4a6 - Browse repository at this point
Copy the full SHA 215b4a6View commit details -
Configuration menu - View commit details
-
Copy full SHA for 8364c3e - Browse repository at this point
Copy the full SHA 8364c3eView commit details -
feat: add BitVec.neg_neg (leanprover#4977)
.. as well as neg_neq_iff_neq_neg. --------- Co-authored-by: Henrik Böving <hargonix@gmail.com>
Configuration menu - View commit details
-
Copy full SHA for 37f9063 - Browse repository at this point
Copy the full SHA 37f9063View commit details -
chore: fix typo in hash code for
Expr
equality test (leanprover#4990)We observed a small performance improvement at https://github.com/leanprover/LNSym/blob/proof_size_expt/Proofs/SHA512/Experiments/Sym30.lean Before: 2.65s After: 2.60s
Configuration menu - View commit details
-
Copy full SHA for 89c3079 - Browse repository at this point
Copy the full SHA 89c3079View commit details -
fix: naming convention for
UInt
lemmas (leanprover#4514)Closes leanprover#4513 --------- Co-authored-by: Kim Morrison <kim@tqft.net>
Configuration menu - View commit details
-
Copy full SHA for 759ece7 - Browse repository at this point
Copy the full SHA 759ece7View commit details -
feat: add BitVec.[sshiftRight/shiftLeft]_*_distrib (leanprover#4951)
After having added already `BitVec.ushiftRight_*_distrib`in leanprover#4667 for ushiftRight, this PR now completes the `*_distrib` theorems for shift.
Configuration menu - View commit details
-
Copy full SHA for dfe493d - Browse repository at this point
Copy the full SHA dfe493dView commit details -
Configuration menu - View commit details
-
Copy full SHA for 23d898c - Browse repository at this point
Copy the full SHA 23d898cView commit details -
Configuration menu - View commit details
-
Copy full SHA for fc56158 - Browse repository at this point
Copy the full SHA fc56158View commit details -
chore: when a linter crashes, prefix its name (leanprover#4967)
Helpful for diagnosing which linter is failing, c.f. [recent problem](https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/quote4/near/457349304) in quote4.
Configuration menu - View commit details
-
Copy full SHA for 0a7af63 - Browse repository at this point
Copy the full SHA 0a7af63View commit details -
Configuration menu - View commit details
-
Copy full SHA for 12ca422 - Browse repository at this point
Copy the full SHA 12ca422View commit details -
feat: add BitVec.toNat_[udiv|umod] and [udiv|umod]_eq
Co-authored-by: Siddharth <siddu.druid@gmail.com>
Configuration menu - View commit details
-
Copy full SHA for 92271ae - Browse repository at this point
Copy the full SHA 92271aeView commit details -
Configuration menu - View commit details
-
Copy full SHA for 01a2342 - Browse repository at this point
Copy the full SHA 01a2342View commit details -
fix: handle SIGBUS when looking for stack overflows (leanprover#4971)
Without this change, a stack overflow on Mac OS during tactic execution can lead to the message: terminated by signal SIGBUS (Misaligned address error) This comes from `lean_alloc_small`. With the change, the process instead terminates with the more accurate and actionable: Stack overflow detected. Aborting.
Configuration menu - View commit details
-
Copy full SHA for ecd3aa4 - Browse repository at this point
Copy the full SHA ecd3aa4View commit details -
fix: reduce default max depth for ext tactic (leanprover#4996)
The prior default of 1000000 could not be achieved in practice, because the stack would overflow after around 5000 recursive invocations. This meant that a poorly-chosen @[ext] lemma could crash Lean. Talking to Mathlib users, it seems that 10 would be a very large number in practice, so a default limit of 100 should not change successful uses. But it does make it much easier to diagnose and recover from poor choices of @[ext] lemmas.
Configuration menu - View commit details
-
Copy full SHA for 5c182bd - Browse repository at this point
Copy the full SHA 5c182bdView commit details -
Update src/Init/Data/BitVec/Lemmas.lean
Co-authored-by: Atticus Kuhn <52258164+AtticusKuhn@users.noreply.github.com>
Configuration menu - View commit details
-
Copy full SHA for 6fbe2ac - Browse repository at this point
Copy the full SHA 6fbe2acView commit details -
Configuration menu - View commit details
-
Copy full SHA for da9d44d - Browse repository at this point
Copy the full SHA da9d44dView commit details -
Configuration menu - View commit details
-
Copy full SHA for 8d12dd8 - Browse repository at this point
Copy the full SHA 8d12dd8View commit details -
Configuration menu - View commit details
-
Copy full SHA for 9d0302e - Browse repository at this point
Copy the full SHA 9d0302eView commit details -
Configuration menu - View commit details
-
Copy full SHA for bbb448c - Browse repository at this point
Copy the full SHA bbb448cView commit details -
Configuration menu - View commit details
-
Copy full SHA for adc7995 - Browse repository at this point
Copy the full SHA adc7995View commit details -
Configuration menu - View commit details
-
Copy full SHA for c5114c9 - Browse repository at this point
Copy the full SHA c5114c9View commit details -
feat: output panics into Lean's redirected stderr (leanprover#4952)
...unless we are about to kill the process anyway (which is not the default) Ensures panics are visible as regular messages in the language server and properly ordered in relation to other messages on the cmdline
Configuration menu - View commit details
-
Copy full SHA for dd4e26f - Browse repository at this point
Copy the full SHA dd4e26fView commit details -
Configuration menu - View commit details
-
Copy full SHA for c237c1f - Browse repository at this point
Copy the full SHA c237c1fView commit details -
feat:
Std.Sat.AIG
(leanprover#4953)Step 2/~7 in upstreaming LeanSAT. --------- Co-authored-by: Tobias Grosser <tobias@grosser.es> Co-authored-by: Siddharth <siddu.druid@gmail.com> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
Configuration menu - View commit details
-
Copy full SHA for dc3eccd - Browse repository at this point
Copy the full SHA dc3eccdView commit details -
chore: upgrade cache action to silence warnings (leanprover#5003)
According to the release notes of cache this should not break anything as they merely upgraded the node version.
Configuration menu - View commit details
-
Copy full SHA for ecb3579 - Browse repository at this point
Copy the full SHA ecb3579View commit details -
fix: check is valid structure projection when pretty printing (leanpr…
…over#4982) For structure projections, the pretty printer assumed that the expression was type correct. Now it checks that the object being projected is of the correct type. Such terms appear in type mismatch errors. Also, fixes and improves `#print` for structures. The types of projections now use MessageData (so are now hoverable), and the type of `self` is now the correct type. Closes leanprover#4670
Configuration menu - View commit details
-
Copy full SHA for 7cd406f - Browse repository at this point
Copy the full SHA 7cd406fView commit details -
perf: avoid MT marking environment in language processor (leanprover#…
…5004) leanprover#4976 moved resolution of a promise to an earlier point, but that led to object being marked MT earlier, so we need to move the code that minimizes those objects earlier too to revert the performance regression.
Configuration menu - View commit details
-
Copy full SHA for f3e7b45 - Browse repository at this point
Copy the full SHA f3e7b45View commit details
Commits on Aug 13, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 5bc6496 - Browse repository at this point
Copy the full SHA 5bc6496View commit details -
Configuration menu - View commit details
-
Copy full SHA for 041b80a - Browse repository at this point
Copy the full SHA 041b80aView commit details -
Configuration menu - View commit details
-
Copy full SHA for 74f9dea - Browse repository at this point
Copy the full SHA 74f9deaView commit details -
Configuration menu - View commit details
-
Copy full SHA for 11be29e - Browse repository at this point
Copy the full SHA 11be29eView commit details -
refactor: state
WellFoundedRelation Nat
using<
, notNat.lt
(le……anprover#5012) as that’s the simp normal form.
Configuration menu - View commit details
-
Copy full SHA for 861ef27 - Browse repository at this point
Copy the full SHA 861ef27View commit details -
Configuration menu - View commit details
-
Copy full SHA for 5a5415d - Browse repository at this point
Copy the full SHA 5a5415dView commit details