mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-19 03:14:08 +00:00
Compare commits
10 Commits
change_arr
...
array_take
| Author | SHA1 | Date | |
|---|---|---|---|
|
f77428252c | ||
|
|
60690665d5 | ||
|
|
538c91c569 | ||
|
|
02baaa42ff | ||
|
|
e573676db1 | ||
|
|
4dab6a108c | ||
|
|
a4d521cf96 | ||
|
|
99070bf304 | ||
|
|
93dd6f2b36 | ||
|
|
c61ced3f15 |
310
RELEASES.md
310
RELEASES.md
@@ -21,7 +21,315 @@ Release candidate, release notes will be copied from the branch `releases/v4.14.
|
||||
v4.13.0
|
||||
----------
|
||||
|
||||
Release candidate, release notes will be copied from the branch `releases/v4.13.0` once completed.
|
||||
**Full Changelog**: https://github.com/leanprover/lean4/compare/v4.12.0...v4.13.0
|
||||
|
||||
### Language features, tactics, and metaprograms
|
||||
|
||||
* `structure` command
|
||||
* [#5511](https://github.com/leanprover/lean4/pull/5511) allows structure parents to be type synonyms.
|
||||
* [#5531](https://github.com/leanprover/lean4/pull/5531) allows default values for structure fields to be noncomputable.
|
||||
|
||||
* `rfl` and `apply_rfl` tactics
|
||||
* [#3714](https://github.com/leanprover/lean4/pull/3714), [#3718](https://github.com/leanprover/lean4/pull/3718) improve the `rfl` tactic and give better error messages.
|
||||
* [#3772](https://github.com/leanprover/lean4/pull/3772) makes `rfl` no longer use kernel defeq for ground terms.
|
||||
* [#5329](https://github.com/leanprover/lean4/pull/5329) tags `Iff.refl` with `@[refl]` (@Parcly-Taxel)
|
||||
* [#5359](https://github.com/leanprover/lean4/pull/5359) ensures that the `rfl` tactic tries `Iff.rfl` (@Parcly-Taxel)
|
||||
|
||||
* `unfold` tactic
|
||||
* [#4834](https://github.com/leanprover/lean4/pull/4834) let `unfold` do zeta-delta reduction of local definitions, incorporating functionality of the Mathlib `unfold_let` tactic.
|
||||
|
||||
* `omega` tactic
|
||||
* [#5382](https://github.com/leanprover/lean4/pull/5382) fixes spurious error in [#5315](https://github.com/leanprover/lean4/issues/5315)
|
||||
* [#5523](https://github.com/leanprover/lean4/pull/5523) supports `Int.toNat`
|
||||
|
||||
* `simp` tactic
|
||||
* [#5479](https://github.com/leanprover/lean4/pull/5479) lets `simp` apply rules with higher-order patterns.
|
||||
|
||||
* `induction` tactic
|
||||
* [#5494](https://github.com/leanprover/lean4/pull/5494) fixes `induction`’s "pre-tactic" block to always be indented, avoiding unintended uses of it.
|
||||
|
||||
* `ac_nf` tactic
|
||||
* [#5524](https://github.com/leanprover/lean4/pull/5524) adds `ac_nf`, a counterpart to `ac_rfl`, for normalizing expressions with respect to associativity and commutativity. Tests it with `BitVec` expressions.
|
||||
|
||||
* `bv_decide`
|
||||
* [#5211](https://github.com/leanprover/lean4/pull/5211) makes `extractLsb'` the primitive `bv_decide` understands, rather than `extractLsb` (@alexkeizer)
|
||||
* [#5365](https://github.com/leanprover/lean4/pull/5365) adds `bv_decide` diagnoses.
|
||||
* [#5375](https://github.com/leanprover/lean4/pull/5375) adds `bv_decide` normalization rules for `ofBool (a.getLsbD i)` and `ofBool a[i]` (@alexkeizer)
|
||||
* [#5423](https://github.com/leanprover/lean4/pull/5423) enhances the rewriting rules of `bv_decide`
|
||||
* [#5433](https://github.com/leanprover/lean4/pull/5433) presents the `bv_decide` counterexample at the API
|
||||
* [#5484](https://github.com/leanprover/lean4/pull/5484) handles `BitVec.ofNat` with `Nat` fvars in `bv_decide`
|
||||
* [#5506](https://github.com/leanprover/lean4/pull/5506), [#5507](https://github.com/leanprover/lean4/pull/5507) add `bv_normalize` rules.
|
||||
* [#5568](https://github.com/leanprover/lean4/pull/5568) generalize the `bv_normalize` pipeline to support more general preprocessing passes
|
||||
* [#5573](https://github.com/leanprover/lean4/pull/5573) gets `bv_normalize` up-to-date with the current `BitVec` rewrites
|
||||
* Cleanups: [#5408](https://github.com/leanprover/lean4/pull/5408), [#5493](https://github.com/leanprover/lean4/pull/5493), [#5578](https://github.com/leanprover/lean4/pull/5578)
|
||||
|
||||
|
||||
* Elaboration improvements
|
||||
* [#5266](https://github.com/leanprover/lean4/pull/5266) preserve order of overapplied arguments in `elab_as_elim` procedure.
|
||||
* [#5510](https://github.com/leanprover/lean4/pull/5510) generalizes `elab_as_elim` to allow arbitrary motive applications.
|
||||
* [#5283](https://github.com/leanprover/lean4/pull/5283), [#5512](https://github.com/leanprover/lean4/pull/5512) refine how named arguments suppress explicit arguments. Breaking change: some previously omitted explicit arguments may need explicit `_` arguments now.
|
||||
* [#5376](https://github.com/leanprover/lean4/pull/5376) modifies projection instance binder info for instances, making parameters that are instance implicit in the type be implicit.
|
||||
* [#5402](https://github.com/leanprover/lean4/pull/5402) localizes universe metavariable errors to `let` bindings and `fun` binders if possible. Makes "cannot synthesize metavariable" errors take precedence over unsolved universe level errors.
|
||||
* [#5419](https://github.com/leanprover/lean4/pull/5419) must not reduce `ite` in the discriminant of `match`-expression when reducibility setting is `.reducible`
|
||||
* [#5474](https://github.com/leanprover/lean4/pull/5474) have autoparams report parameter/field on failure
|
||||
* [#5530](https://github.com/leanprover/lean4/pull/5530) makes automatic instance names about types with hygienic names be hygienic.
|
||||
|
||||
* Deriving handlers
|
||||
* [#5432](https://github.com/leanprover/lean4/pull/5432) makes `Repr` deriving instance handle explicit type parameters
|
||||
|
||||
* Functional induction
|
||||
* [#5364](https://github.com/leanprover/lean4/pull/5364) adds more equalities in context, more careful cleanup.
|
||||
|
||||
* Linters
|
||||
* [#5335](https://github.com/leanprover/lean4/pull/5335) fixes the unused variables linter complaining about match/tactic combinations
|
||||
* [#5337](https://github.com/leanprover/lean4/pull/5337) fixes the unused variables linter complaining about some wildcard patterns
|
||||
|
||||
* Other fixes
|
||||
* [#4768](https://github.com/leanprover/lean4/pull/4768) fixes a parse error when `..` appears with a `.` on the next line
|
||||
|
||||
* Metaprogramming
|
||||
* [#3090](https://github.com/leanprover/lean4/pull/3090) handles level parameters in `Meta.evalExpr` (@eric-wieser)
|
||||
* [#5401](https://github.com/leanprover/lean4/pull/5401) instance for `Inhabited (TacticM α)` (@alexkeizer)
|
||||
* [#5412](https://github.com/leanprover/lean4/pull/5412) expose Kernel.check for debugging purposes
|
||||
* [#5556](https://github.com/leanprover/lean4/pull/5556) improves the "invalid projection" type inference error in `inferType`.
|
||||
* [#5587](https://github.com/leanprover/lean4/pull/5587) allows `MVarId.assertHypotheses` to set `BinderInfo` and `LocalDeclKind`.
|
||||
* [#5588](https://github.com/leanprover/lean4/pull/5588) adds `MVarId.tryClearMany'`, a variant of `MVarId.tryClearMany`.
|
||||
|
||||
|
||||
|
||||
### Language server, widgets, and IDE extensions
|
||||
|
||||
* [#5205](https://github.com/leanprover/lean4/pull/5205) decreases the latency of auto-completion in tactic blocks.
|
||||
* [#5237](https://github.com/leanprover/lean4/pull/5237) fixes symbol occurrence highlighting in VS Code not highlighting occurrences when moving the text cursor into the identifier from the right.
|
||||
* [#5257](https://github.com/leanprover/lean4/pull/5257) fixes several instances of incorrect auto-completions being reported.
|
||||
* [#5299](https://github.com/leanprover/lean4/pull/5299) allows auto-completion to report completions for global identifiers when the elaborator fails to provide context-specific auto-completions.
|
||||
* [#5312](https://github.com/leanprover/lean4/pull/5312) fixes the server breaking when changing whitespace after the module header.
|
||||
* [#5322](https://github.com/leanprover/lean4/pull/5322) fixes several instances of auto-completion reporting non-existent namespaces.
|
||||
* [#5428](https://github.com/leanprover/lean4/pull/5428) makes sure to always report some recent file range as progress when waiting for elaboration.
|
||||
|
||||
|
||||
### Pretty printing
|
||||
|
||||
* [#4979](https://github.com/leanprover/lean4/pull/4979) make pretty printer escape identifiers that are tokens.
|
||||
* [#5389](https://github.com/leanprover/lean4/pull/5389) makes formatter use the current token table.
|
||||
* [#5513](https://github.com/leanprover/lean4/pull/5513) use breakable instead of unbreakable whitespace when formatting tokens.
|
||||
|
||||
|
||||
### Library
|
||||
|
||||
* [#5222](https://github.com/leanprover/lean4/pull/5222) reduces allocations in `Json.compress`.
|
||||
* [#5231](https://github.com/leanprover/lean4/pull/5231) upstreams `Zero` and `NeZero`
|
||||
* [#5292](https://github.com/leanprover/lean4/pull/5292) refactors `Lean.Elab.Deriving.FromToJson` (@arthur-adjedj)
|
||||
* [#5415](https://github.com/leanprover/lean4/pull/5415) implements `Repr Empty` (@TomasPuverle)
|
||||
* [#5421](https://github.com/leanprover/lean4/pull/5421) implements `To/FromJSON Empty` (@TomasPuverle)
|
||||
|
||||
* Logic
|
||||
* [#5263](https://github.com/leanprover/lean4/pull/5263) allows simplifying `dite_not`/`decide_not` with only `Decidable (¬p)`.
|
||||
* [#5268](https://github.com/leanprover/lean4/pull/5268) fixes binders on `ite_eq_left_iff`
|
||||
* [#5284](https://github.com/leanprover/lean4/pull/5284) turns off `Inhabited (Sum α β)` instances
|
||||
* [#5355](https://github.com/leanprover/lean4/pull/5355) adds simp lemmas for `LawfulBEq`
|
||||
* [#5374](https://github.com/leanprover/lean4/pull/5374) add `Nonempty` instances for products, allowing more `partial` functions to elaborate successfully
|
||||
* [#5447](https://github.com/leanprover/lean4/pull/5447) updates Pi instance names
|
||||
* [#5454](https://github.com/leanprover/lean4/pull/5454) makes some instance arguments implicit
|
||||
* [#5456](https://github.com/leanprover/lean4/pull/5456) adds `heq_comm`
|
||||
* [#5529](https://github.com/leanprover/lean4/pull/5529) moves `@[simp]` from `exists_prop'` to `exists_prop`
|
||||
|
||||
* `Bool`
|
||||
* [#5228](https://github.com/leanprover/lean4/pull/5228) fills gaps in Bool lemmas
|
||||
* [#5332](https://github.com/leanprover/lean4/pull/5332) adds notation `^^` for Bool.xor
|
||||
* [#5351](https://github.com/leanprover/lean4/pull/5351) removes `_root_.and` (and or/not/xor) and instead exports/uses `Bool.and` (etc.).
|
||||
|
||||
* `BitVec`
|
||||
* [#5240](https://github.com/leanprover/lean4/pull/5240) removes BitVec simps with complicated RHS
|
||||
* [#5247](https://github.com/leanprover/lean4/pull/5247) `BitVec.getElem_zeroExtend`
|
||||
* [#5248](https://github.com/leanprover/lean4/pull/5248) simp lemmas for BitVec, improving confluence
|
||||
* [#5249](https://github.com/leanprover/lean4/pull/5249) removes `@[simp]` from some BitVec lemmas
|
||||
* [#5252](https://github.com/leanprover/lean4/pull/5252) changes `BitVec.intMin/Max` from abbrev to def
|
||||
* [#5278](https://github.com/leanprover/lean4/pull/5278) adds `BitVec.getElem_truncate` (@tobiasgrosser)
|
||||
* [#5281](https://github.com/leanprover/lean4/pull/5281) adds udiv/umod bitblasting for `bv_decide` (@bollu)
|
||||
* [#5297](https://github.com/leanprover/lean4/pull/5297) `BitVec` unsigned order theoretic results
|
||||
* [#5313](https://github.com/leanprover/lean4/pull/5313) adds more basic BitVec ordering theory for UInt
|
||||
* [#5314](https://github.com/leanprover/lean4/pull/5314) adds `toNat_sub_of_le` (@bollu)
|
||||
* [#5357](https://github.com/leanprover/lean4/pull/5357) adds `BitVec.truncate` lemmas
|
||||
* [#5358](https://github.com/leanprover/lean4/pull/5358) introduces `BitVec.setWidth` to unify zeroExtend and truncate (@tobiasgrosser)
|
||||
* [#5361](https://github.com/leanprover/lean4/pull/5361) some BitVec GetElem lemmas
|
||||
* [#5385](https://github.com/leanprover/lean4/pull/5385) adds `BitVec.ofBool_[and|or|xor]_ofBool` theorems (@tobiasgrosser)
|
||||
* [#5404](https://github.com/leanprover/lean4/pull/5404) more of `BitVec.getElem_*` (@tobiasgrosser)
|
||||
* [#5410](https://github.com/leanprover/lean4/pull/5410) BitVec analogues of `Nat.{mul_two, two_mul, mul_succ, succ_mul}` (@bollu)
|
||||
* [#5411](https://github.com/leanprover/lean4/pull/5411) `BitVec.toNat_{add,sub,mul_of_lt}` for BitVector non-overflow reasoning (@bollu)
|
||||
* [#5413](https://github.com/leanprover/lean4/pull/5413) adds `_self`, `_zero`, and `_allOnes` for `BitVec.[and|or|xor]` (@tobiasgrosser)
|
||||
* [#5416](https://github.com/leanprover/lean4/pull/5416) adds LawCommIdentity + IdempotentOp for `BitVec.[and|or|xor]` (@tobiasgrosser)
|
||||
* [#5418](https://github.com/leanprover/lean4/pull/5418) decidable quantifers for BitVec
|
||||
* [#5450](https://github.com/leanprover/lean4/pull/5450) adds `BitVec.toInt_[intMin|neg|neg_of_ne_intMin]` (@tobiasgrosser)
|
||||
* [#5459](https://github.com/leanprover/lean4/pull/5459) missing BitVec lemmas
|
||||
* [#5469](https://github.com/leanprover/lean4/pull/5469) adds `BitVec.[not_not, allOnes_shiftLeft_or_shiftLeft, allOnes_shiftLeft_and_shiftLeft]` (@luisacicolini)
|
||||
* [#5478](https://github.com/leanprover/lean4/pull/5478) adds `BitVec.(shiftLeft_add_distrib, shiftLeft_ushiftRight)` (@luisacicolini)
|
||||
* [#5487](https://github.com/leanprover/lean4/pull/5487) adds `sdiv_eq`, `smod_eq` to allow `sdiv`/`smod` bitblasting (@bollu)
|
||||
* [#5491](https://github.com/leanprover/lean4/pull/5491) adds `BitVec.toNat_[abs|sdiv|smod]` (@tobiasgrosser)
|
||||
* [#5492](https://github.com/leanprover/lean4/pull/5492) `BitVec.(not_sshiftRight, not_sshiftRight_not, getMsb_not, msb_not)` (@luisacicolini)
|
||||
* [#5499](https://github.com/leanprover/lean4/pull/5499) `BitVec.Lemmas` - drop non-terminal simps (@tobiasgrosser)
|
||||
* [#5505](https://github.com/leanprover/lean4/pull/5505) unsimps `BitVec.divRec_succ'`
|
||||
* [#5508](https://github.com/leanprover/lean4/pull/5508) adds `BitVec.getElem_[add|add_add_bool|mul|rotateLeft|rotateRight…` (@tobiasgrosser)
|
||||
* [#5554](https://github.com/leanprover/lean4/pull/5554) adds `Bitvec.[add, sub, mul]_eq_xor` and `width_one_cases` (@luisacicolini)
|
||||
|
||||
* `List`
|
||||
* [#5242](https://github.com/leanprover/lean4/pull/5242) improve naming for `List.mergeSort` lemmas
|
||||
* [#5302](https://github.com/leanprover/lean4/pull/5302) provide `mergeSort` comparator autoParam
|
||||
* [#5373](https://github.com/leanprover/lean4/pull/5373) fix name of `List.length_mergeSort`
|
||||
* [#5377](https://github.com/leanprover/lean4/pull/5377) upstream `map_mergeSort`
|
||||
* [#5378](https://github.com/leanprover/lean4/pull/5378) modify signature of lemmas about `mergeSort`
|
||||
* [#5245](https://github.com/leanprover/lean4/pull/5245) avoid importing `List.Basic` without List.Impl
|
||||
* [#5260](https://github.com/leanprover/lean4/pull/5260) review of List API
|
||||
* [#5264](https://github.com/leanprover/lean4/pull/5264) review of List API
|
||||
* [#5269](https://github.com/leanprover/lean4/pull/5269) remove HashMap's duplicated Pairwise and Sublist
|
||||
* [#5271](https://github.com/leanprover/lean4/pull/5271) remove @[simp] from `List.head_mem` and similar
|
||||
* [#5273](https://github.com/leanprover/lean4/pull/5273) lemmas about `List.attach`
|
||||
* [#5275](https://github.com/leanprover/lean4/pull/5275) reverse direction of `List.tail_map`
|
||||
* [#5277](https://github.com/leanprover/lean4/pull/5277) more `List.attach` lemmas
|
||||
* [#5285](https://github.com/leanprover/lean4/pull/5285) `List.count` lemmas
|
||||
* [#5287](https://github.com/leanprover/lean4/pull/5287) use boolean predicates in `List.filter`
|
||||
* [#5289](https://github.com/leanprover/lean4/pull/5289) `List.mem_ite_nil_left` and analogues
|
||||
* [#5293](https://github.com/leanprover/lean4/pull/5293) cleanup of `List.findIdx` / `List.take` lemmas
|
||||
* [#5294](https://github.com/leanprover/lean4/pull/5294) switch primes on `List.getElem_take`
|
||||
* [#5300](https://github.com/leanprover/lean4/pull/5300) more `List.findIdx` theorems
|
||||
* [#5310](https://github.com/leanprover/lean4/pull/5310) fix `List.all/any` lemmas
|
||||
* [#5311](https://github.com/leanprover/lean4/pull/5311) fix `List.countP` lemmas
|
||||
* [#5316](https://github.com/leanprover/lean4/pull/5316) `List.tail` lemma
|
||||
* [#5331](https://github.com/leanprover/lean4/pull/5331) fix implicitness of `List.getElem_mem`
|
||||
* [#5350](https://github.com/leanprover/lean4/pull/5350) `List.replicate` lemmas
|
||||
* [#5352](https://github.com/leanprover/lean4/pull/5352) `List.attachWith` lemmas
|
||||
* [#5353](https://github.com/leanprover/lean4/pull/5353) `List.head_mem_head?`
|
||||
* [#5360](https://github.com/leanprover/lean4/pull/5360) lemmas about `List.tail`
|
||||
* [#5391](https://github.com/leanprover/lean4/pull/5391) review of `List.erase` / `List.find` lemmas
|
||||
* [#5392](https://github.com/leanprover/lean4/pull/5392) `List.fold` / `attach` lemmas
|
||||
* [#5393](https://github.com/leanprover/lean4/pull/5393) `List.fold` relators
|
||||
* [#5394](https://github.com/leanprover/lean4/pull/5394) lemmas about `List.maximum?`
|
||||
* [#5403](https://github.com/leanprover/lean4/pull/5403) theorems about `List.toArray`
|
||||
* [#5405](https://github.com/leanprover/lean4/pull/5405) reverse direction of `List.set_map`
|
||||
* [#5448](https://github.com/leanprover/lean4/pull/5448) add lemmas about `List.IsPrefix` (@Command-Master)
|
||||
* [#5460](https://github.com/leanprover/lean4/pull/5460) missing `List.set_replicate_self`
|
||||
* [#5518](https://github.com/leanprover/lean4/pull/5518) rename `List.maximum?` to `max?`
|
||||
* [#5519](https://github.com/leanprover/lean4/pull/5519) upstream `List.fold` lemmas
|
||||
* [#5520](https://github.com/leanprover/lean4/pull/5520) restore `@[simp]` on `List.getElem_mem` etc.
|
||||
* [#5521](https://github.com/leanprover/lean4/pull/5521) List simp fixes
|
||||
* [#5550](https://github.com/leanprover/lean4/pull/5550) `List.unattach` and simp lemmas
|
||||
* [#5594](https://github.com/leanprover/lean4/pull/5594) induction-friendly `List.min?_cons`
|
||||
|
||||
* `Array`
|
||||
* [#5246](https://github.com/leanprover/lean4/pull/5246) cleanup imports of Array.Lemmas
|
||||
* [#5255](https://github.com/leanprover/lean4/pull/5255) split Init.Data.Array.Lemmas for better bootstrapping
|
||||
* [#5288](https://github.com/leanprover/lean4/pull/5288) rename `Array.data` to `Array.toList`
|
||||
* [#5303](https://github.com/leanprover/lean4/pull/5303) cleanup of `List.getElem_append` variants
|
||||
* [#5304](https://github.com/leanprover/lean4/pull/5304) `Array.not_mem_empty`
|
||||
* [#5400](https://github.com/leanprover/lean4/pull/5400) reorganization in Array/Basic
|
||||
* [#5420](https://github.com/leanprover/lean4/pull/5420) make `Array` functions either semireducible or use structural recursion
|
||||
* [#5422](https://github.com/leanprover/lean4/pull/5422) refactor `DecidableEq (Array α)`
|
||||
* [#5452](https://github.com/leanprover/lean4/pull/5452) refactor of Array
|
||||
* [#5458](https://github.com/leanprover/lean4/pull/5458) cleanup of Array docstrings after refactor
|
||||
* [#5461](https://github.com/leanprover/lean4/pull/5461) restore `@[simp]` on `Array.swapAt!_def`
|
||||
* [#5465](https://github.com/leanprover/lean4/pull/5465) improve Array GetElem lemmas
|
||||
* [#5466](https://github.com/leanprover/lean4/pull/5466) `Array.foldX` lemmas
|
||||
* [#5472](https://github.com/leanprover/lean4/pull/5472) @[simp] lemmas about `List.toArray`
|
||||
* [#5485](https://github.com/leanprover/lean4/pull/5485) reverse simp direction for `toArray_concat`
|
||||
* [#5514](https://github.com/leanprover/lean4/pull/5514) `Array.eraseReps`
|
||||
* [#5515](https://github.com/leanprover/lean4/pull/5515) upstream `Array.qsortOrd`
|
||||
* [#5516](https://github.com/leanprover/lean4/pull/5516) upstream `Subarray.empty`
|
||||
* [#5526](https://github.com/leanprover/lean4/pull/5526) fix name of `Array.length_toList`
|
||||
* [#5527](https://github.com/leanprover/lean4/pull/5527) reduce use of deprecated lemmas in Array
|
||||
* [#5534](https://github.com/leanprover/lean4/pull/5534) cleanup of Array GetElem lemmas
|
||||
* [#5536](https://github.com/leanprover/lean4/pull/5536) fix `Array.modify` lemmas
|
||||
* [#5551](https://github.com/leanprover/lean4/pull/5551) upstream `Array.flatten` lemmas
|
||||
* [#5552](https://github.com/leanprover/lean4/pull/5552) switch obvious cases of array "bang"`[]!` indexing to rely on hypothesis (@TomasPuverle)
|
||||
* [#5577](https://github.com/leanprover/lean4/pull/5577) add missing simp to `Array.size_feraseIdx`
|
||||
* [#5586](https://github.com/leanprover/lean4/pull/5586) `Array/Option.unattach`
|
||||
|
||||
* `Option`
|
||||
* [#5272](https://github.com/leanprover/lean4/pull/5272) remove @[simp] from `Option.pmap/pbind` and add simp lemmas
|
||||
* [#5307](https://github.com/leanprover/lean4/pull/5307) restoring Option simp confluence
|
||||
* [#5354](https://github.com/leanprover/lean4/pull/5354) remove @[simp] from `Option.bind_map`
|
||||
* [#5532](https://github.com/leanprover/lean4/pull/5532) `Option.attach`
|
||||
* [#5539](https://github.com/leanprover/lean4/pull/5539) fix explicitness of `Option.mem_toList`
|
||||
|
||||
* `Nat`
|
||||
* [#5241](https://github.com/leanprover/lean4/pull/5241) add @[simp] to `Nat.add_eq_zero_iff`
|
||||
* [#5261](https://github.com/leanprover/lean4/pull/5261) Nat bitwise lemmas
|
||||
* [#5262](https://github.com/leanprover/lean4/pull/5262) `Nat.testBit_add_one` should not be a global simp lemma
|
||||
* [#5267](https://github.com/leanprover/lean4/pull/5267) protect some Nat bitwise theorems
|
||||
* [#5305](https://github.com/leanprover/lean4/pull/5305) rename Nat bitwise lemmas
|
||||
* [#5306](https://github.com/leanprover/lean4/pull/5306) add `Nat.self_sub_mod` lemma
|
||||
* [#5503](https://github.com/leanprover/lean4/pull/5503) restore @[simp] to upstreamed `Nat.lt_off_iff`
|
||||
|
||||
* `Int`
|
||||
* [#5301](https://github.com/leanprover/lean4/pull/5301) rename `Int.div/mod` to `Int.tdiv/tmod`
|
||||
* [#5320](https://github.com/leanprover/lean4/pull/5320) add `ediv_nonneg_of_nonpos_of_nonpos` to DivModLemmas (@sakehl)
|
||||
|
||||
* `Fin`
|
||||
* [#5250](https://github.com/leanprover/lean4/pull/5250) missing lemma about `Fin.ofNat'`
|
||||
* [#5356](https://github.com/leanprover/lean4/pull/5356) `Fin.ofNat'` uses `NeZero`
|
||||
* [#5379](https://github.com/leanprover/lean4/pull/5379) remove some @[simp]s from Fin lemmas
|
||||
* [#5380](https://github.com/leanprover/lean4/pull/5380) missing Fin @[simp] lemmas
|
||||
|
||||
* `HashMap`
|
||||
* [#5244](https://github.com/leanprover/lean4/pull/5244) (`DHashMap`|`HashMap`|`HashSet`).(`getKey?`|`getKey`|`getKey!`|`getKeyD`)
|
||||
* [#5362](https://github.com/leanprover/lean4/pull/5362) remove the last use of `Lean.(HashSet|HashMap)`
|
||||
* [#5369](https://github.com/leanprover/lean4/pull/5369) `HashSet.ofArray`
|
||||
* [#5370](https://github.com/leanprover/lean4/pull/5370) `HashSet.partition`
|
||||
* [#5581](https://github.com/leanprover/lean4/pull/5581) `Singleton`/`Insert`/`Union` instances for `HashMap`/`Set`
|
||||
* [#5582](https://github.com/leanprover/lean4/pull/5582) `HashSet.all`/`any`
|
||||
* [#5590](https://github.com/leanprover/lean4/pull/5590) adding `Insert`/`Singleton`/`Union` instances for `HashMap`/`Set.Raw`
|
||||
* [#5591](https://github.com/leanprover/lean4/pull/5591) `HashSet.Raw.all/any`
|
||||
|
||||
* `Monads`
|
||||
* [#5463](https://github.com/leanprover/lean4/pull/5463) upstream some monad lemmas
|
||||
* [#5464](https://github.com/leanprover/lean4/pull/5464) adjust simp attributes on monad lemmas
|
||||
* [#5522](https://github.com/leanprover/lean4/pull/5522) more monadic simp lemmas
|
||||
|
||||
* Simp lemma cleanup
|
||||
* [#5251](https://github.com/leanprover/lean4/pull/5251) remove redundant simp annotations
|
||||
* [#5253](https://github.com/leanprover/lean4/pull/5253) remove Int simp lemmas that can't fire
|
||||
* [#5254](https://github.com/leanprover/lean4/pull/5254) variables appearing on both sides of an iff should be implicit
|
||||
* [#5381](https://github.com/leanprover/lean4/pull/5381) cleaning up redundant simp lemmas
|
||||
|
||||
|
||||
### Compiler, runtime, and FFI
|
||||
|
||||
* [#4685](https://github.com/leanprover/lean4/pull/4685) fixes a typo in the C `run_new_frontend` signature
|
||||
* [#4729](https://github.com/leanprover/lean4/pull/4729) has IR checker suggest using `noncomputable`
|
||||
* [#5143](https://github.com/leanprover/lean4/pull/5143) adds a shared library for Lake
|
||||
* [#5437](https://github.com/leanprover/lean4/pull/5437) removes (syntactically) duplicate imports (@euprunin)
|
||||
* [#5462](https://github.com/leanprover/lean4/pull/5462) updates `src/lake/lakefile.toml` to the adjusted Lake build process
|
||||
* [#5541](https://github.com/leanprover/lean4/pull/5541) removes new shared libs before build to better support Windows
|
||||
* [#5558](https://github.com/leanprover/lean4/pull/5558) make `lean.h` compile with MSVC (@kant2002)
|
||||
* [#5564](https://github.com/leanprover/lean4/pull/5564) removes non-conforming size-0 arrays (@eric-wieser)
|
||||
|
||||
|
||||
### Lake
|
||||
* Reservoir build cache. Lake will now attempt to fetch a pre-built copy of the package from Reservoir before building it. This is only enabled for packages in the leanprover or leanprover-community organizations on versions indexed by Reservoir. Users can force Lake to build packages from the source by passing --no-cache on the CLI or by setting the LAKE_NO_CACHE environment variable to true. [#5486](https://github.com/leanprover/lean4/pull/5486), [#5572](https://github.com/leanprover/lean4/pull/5572), [#5583](https://github.com/leanprover/lean4/pull/5583), [#5600](https://github.com/leanprover/lean4/pull/5600), [#5641](https://github.com/leanprover/lean4/pull/5641), [#5642](https://github.com/leanprover/lean4/pull/5642).
|
||||
* [#5504](https://github.com/leanprover/lean4/pull/5504) lake new and lake init now produce TOML configurations by default.
|
||||
* [#5878](https://github.com/leanprover/lean4/pull/5878) fixes a serious issue where Lake would delete path dependencies when attempting to cleanup a dependency required with an incorrect name.
|
||||
|
||||
* **Breaking changes**
|
||||
* [#5641](https://github.com/leanprover/lean4/pull/5641) A Lake build of target within a package will no longer build a package's dependencies package-level extra target dependencies. At the technical level, a package's extraDep facet no longer transitively builds its dependencies’ extraDep facets (which include their extraDepTargets).
|
||||
|
||||
### Documentation fixes
|
||||
|
||||
* [#3918](https://github.com/leanprover/lean4/pull/3918) `@[builtin_doc]` attribute (@digama0)
|
||||
* [#4305](https://github.com/leanprover/lean4/pull/4305) explains the borrow syntax (@eric-wieser)
|
||||
* [#5349](https://github.com/leanprover/lean4/pull/5349) adds documentation for `groupBy.loop` (@vihdzp)
|
||||
* [#5473](https://github.com/leanprover/lean4/pull/5473) fixes typo in `BitVec.mul` docstring (@llllvvuu)
|
||||
* [#5476](https://github.com/leanprover/lean4/pull/5476) fixes typos in `Lean.MetavarContext`
|
||||
* [#5481](https://github.com/leanprover/lean4/pull/5481) removes mention of `Lean.withSeconds` (@alexkeizer)
|
||||
* [#5497](https://github.com/leanprover/lean4/pull/5497) updates documentation and tests for `toUIntX` functions (@TomasPuverle)
|
||||
* [#5087](https://github.com/leanprover/lean4/pull/5087) mentions that `inferType` does not ensure type correctness
|
||||
* Many fixes to spelling across the doc-strings, (@euprunin): [#5425](https://github.com/leanprover/lean4/pull/5425) [#5426](https://github.com/leanprover/lean4/pull/5426) [#5427](https://github.com/leanprover/lean4/pull/5427) [#5430](https://github.com/leanprover/lean4/pull/5430) [#5431](https://github.com/leanprover/lean4/pull/5431) [#5434](https://github.com/leanprover/lean4/pull/5434) [#5435](https://github.com/leanprover/lean4/pull/5435) [#5436](https://github.com/leanprover/lean4/pull/5436) [#5438](https://github.com/leanprover/lean4/pull/5438) [#5439](https://github.com/leanprover/lean4/pull/5439) [#5440](https://github.com/leanprover/lean4/pull/5440) [#5599](https://github.com/leanprover/lean4/pull/5599)
|
||||
|
||||
### Changes to CI
|
||||
|
||||
* [#5343](https://github.com/leanprover/lean4/pull/5343) allows addition of `release-ci` label via comment (@thorimur)
|
||||
* [#5344](https://github.com/leanprover/lean4/pull/5344) sets check level correctly during workflow (@thorimur)
|
||||
* [#5444](https://github.com/leanprover/lean4/pull/5444) Mathlib's `lean-pr-testing-NNNN` branches should use Batteries' `lean-pr-testing-NNNN` branches
|
||||
* [#5489](https://github.com/leanprover/lean4/pull/5489) commit `lake-manifest.json` when updating `lean-pr-testing` branches
|
||||
* [#5490](https://github.com/leanprover/lean4/pull/5490) use separate secrets for commenting and branching in `pr-release.yml`
|
||||
|
||||
v4.12.0
|
||||
----------
|
||||
|
||||
@@ -23,7 +23,7 @@ theorem foldlM_eq_foldlM_toList.aux [Monad m]
|
||||
· cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
|
||||
· rename_i i; rw [Nat.succ_add] at H
|
||||
simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
|
||||
rw (occs := .pos [2]) [← List.get_drop_eq_drop _ _ ‹_›]
|
||||
rw (occs := .pos [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
|
||||
rfl
|
||||
· rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
|
||||
|
||||
|
||||
@@ -41,6 +41,6 @@ where
|
||||
getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
|
||||
rfl
|
||||
go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
|
||||
induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.get_drop_eq_drop, *]
|
||||
induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.getElem_cons_drop_succ_eq_drop, *]
|
||||
|
||||
end Array
|
||||
|
||||
@@ -246,7 +246,7 @@ where
|
||||
aux (i r) :
|
||||
mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
|
||||
unfold mapM.map; split
|
||||
· rw [← List.get_drop_eq_drop _ i ‹_›]
|
||||
· rw [← List.getElem_cons_drop_succ_eq_drop ‹_›]
|
||||
simp only [aux (i + 1), map_eq_pure_bind, length_toList, List.foldlM_cons, bind_assoc,
|
||||
pure_bind]
|
||||
rfl
|
||||
@@ -1619,6 +1619,38 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
|
||||
@[simp] theorem toArray_ofFn (f : Fin n → α) : (ofFn f).toArray = Array.ofFn f := by
|
||||
ext <;> simp
|
||||
|
||||
theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) :
|
||||
takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by
|
||||
rw [takeWhile.go, takeWhile.go]
|
||||
simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
|
||||
getElem_toArray, getElem_cons_succ]
|
||||
split
|
||||
rw [takeWhile_go_succ]
|
||||
rfl
|
||||
|
||||
theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
|
||||
Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by
|
||||
induction l generalizing i r with
|
||||
| nil => simp [takeWhile.go]
|
||||
| cons a l ih =>
|
||||
rw [takeWhile.go]
|
||||
cases i with
|
||||
| zero =>
|
||||
simp [takeWhile_go_succ, ih, takeWhile_cons]
|
||||
split <;> simp
|
||||
| succ i =>
|
||||
simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
|
||||
getElem_toArray, getElem_cons_succ, drop_succ_cons]
|
||||
split <;> rename_i h₁
|
||||
· rw [takeWhile_go_succ, ih]
|
||||
rw [← getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons]
|
||||
split <;> simp_all
|
||||
· simp_all [drop_eq_nil_of_le]
|
||||
|
||||
@[simp] theorem takeWhile_toArray (p : α → Bool) (l : List α) :
|
||||
l.toArray.takeWhile p = (l.takeWhile p).toArray := by
|
||||
simp [Array.takeWhile, takeWhile_go_toArray]
|
||||
|
||||
end List
|
||||
|
||||
namespace Array
|
||||
@@ -1629,6 +1661,10 @@ namespace Array
|
||||
@[simp] theorem toList_ofFn (f : Fin n → α) : (Array.ofFn f).toList = List.ofFn f := by
|
||||
apply List.ext_getElem <;> simp
|
||||
|
||||
@[simp] theorem toList_takeWhile (p : α → Bool) (as : Array α) :
|
||||
(as.takeWhile p).toList = as.toList.takeWhile p := by
|
||||
induction as; simp
|
||||
|
||||
end Array
|
||||
|
||||
/-! ### Deprecations -/
|
||||
|
||||
@@ -169,6 +169,13 @@ theorem pmap_ne_nil_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : Li
|
||||
(H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ [] ↔ xs ≠ [] := by
|
||||
simp
|
||||
|
||||
theorem pmap_eq_self {l : List α} {p : α → Prop} (hp : ∀ (a : α), a ∈ l → p a)
|
||||
(f : (a : α) → p a → α) : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a := by
|
||||
rw [pmap_eq_map_attach]
|
||||
conv => lhs; rhs; rw [← attach_map_subtype_val l]
|
||||
rw [map_inj_left]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
theorem attach_eq_nil_iff {l : List α} : l.attach = [] ↔ l = [] :=
|
||||
pmap_eq_nil_iff
|
||||
|
||||
@@ -190,7 +190,7 @@ theorem set_drop {l : List α} {n m : Nat} {a : α} :
|
||||
theorem take_concat_get (l : List α) (i : Nat) (h : i < l.length) :
|
||||
(l.take i).concat l[i] = l.take (i+1) :=
|
||||
Eq.symm <| (append_left_inj _).1 <| (take_append_drop (i+1) l).trans <| by
|
||||
rw [concat_eq_append, append_assoc, singleton_append, get_drop_eq_drop, take_append_drop]
|
||||
rw [concat_eq_append, append_assoc, singleton_append, getElem_cons_drop_succ_eq_drop, take_append_drop]
|
||||
|
||||
@[deprecated take_succ_cons (since := "2024-07-25")]
|
||||
theorem take_cons_succ : (a::as).take (i+1) = a :: as.take i := rfl
|
||||
|
||||
@@ -374,9 +374,15 @@ end choice
|
||||
|
||||
-- See `Init.Data.Option.List` for lemmas about `toList`.
|
||||
|
||||
@[simp] theorem or_some : (some a).or o = some a := rfl
|
||||
@[simp] theorem some_or : (some a).or o = some a := rfl
|
||||
@[simp] theorem none_or : none.or o = o := rfl
|
||||
|
||||
@[deprecated some_or (since := "2024-11-03")] theorem or_some : (some a).or o = some a := rfl
|
||||
|
||||
/-- This will be renamed to `or_some` once the existing deprecated lemma is removed. -/
|
||||
@[simp] theorem or_some' {o : Option α} : o.or (some a) = o.getD a := by
|
||||
cases o <;> rfl
|
||||
|
||||
theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by
|
||||
cases o <;> rfl
|
||||
|
||||
|
||||
@@ -22,6 +22,36 @@ structure Int8 where
|
||||
-/
|
||||
toUInt8 : UInt8
|
||||
|
||||
/--
|
||||
The type of signed 16-bit integers. This type has special support in the
|
||||
compiler to make it actually 16 bits rather than wrapping a `Nat`.
|
||||
-/
|
||||
structure Int16 where
|
||||
/--
|
||||
Obtain the `UInt16` that is 2's complement equivalent to the `Int16`.
|
||||
-/
|
||||
toUInt16 : UInt16
|
||||
|
||||
/--
|
||||
The type of signed 32-bit integers. This type has special support in the
|
||||
compiler to make it actually 32 bits rather than wrapping a `Nat`.
|
||||
-/
|
||||
structure Int32 where
|
||||
/--
|
||||
Obtain the `UInt32` that is 2's complement equivalent to the `Int32`.
|
||||
-/
|
||||
toUInt32 : UInt32
|
||||
|
||||
/--
|
||||
The type of signed 64-bit integers. This type has special support in the
|
||||
compiler to make it actually 64 bits rather than wrapping a `Nat`.
|
||||
-/
|
||||
structure Int64 where
|
||||
/--
|
||||
Obtain the `UInt64` that is 2's complement equivalent to the `Int64`.
|
||||
-/
|
||||
toUInt64 : UInt64
|
||||
|
||||
/-- The size of type `Int8`, that is, `2^8 = 256`. -/
|
||||
abbrev Int8.size : Nat := 256
|
||||
|
||||
@@ -32,12 +62,16 @@ Obtain the `BitVec` that contains the 2's complement representation of the `Int8
|
||||
|
||||
@[extern "lean_int8_of_int"]
|
||||
def Int8.ofInt (i : @& Int) : Int8 := ⟨⟨BitVec.ofInt 8 i⟩⟩
|
||||
@[extern "lean_int8_of_int"]
|
||||
@[extern "lean_int8_of_nat"]
|
||||
def Int8.ofNat (n : @& Nat) : Int8 := ⟨⟨BitVec.ofNat 8 n⟩⟩
|
||||
abbrev Int.toInt8 := Int8.ofInt
|
||||
abbrev Nat.toInt8 := Int8.ofNat
|
||||
@[extern "lean_int8_to_int"]
|
||||
def Int8.toInt (i : Int8) : Int := i.toBitVec.toInt
|
||||
/--
|
||||
This function has the same behavior as `Int.toNat` for negative numbers.
|
||||
If you want to obtain the 2's complement representation use `toBitVec`.
|
||||
-/
|
||||
@[inline] def Int8.toNat (i : Int8) : Nat := i.toInt.toNat
|
||||
@[extern "lean_int8_neg"]
|
||||
def Int8.neg (i : Int8) : Int8 := ⟨⟨-i.toBitVec⟩⟩
|
||||
@@ -58,7 +92,7 @@ def Int8.mul (a b : Int8) : Int8 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
|
||||
@[extern "lean_int8_div"]
|
||||
def Int8.div (a b : Int8) : Int8 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
|
||||
@[extern "lean_int8_mod"]
|
||||
def Int8.mod (a b : Int8) : Int8 := ⟨⟨BitVec.smod a.toBitVec b.toBitVec⟩⟩
|
||||
def Int8.mod (a b : Int8) : Int8 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
|
||||
@[extern "lean_int8_land"]
|
||||
def Int8.land (a b : Int8) : Int8 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
|
||||
@[extern "lean_int8_lor"]
|
||||
@@ -66,9 +100,9 @@ def Int8.lor (a b : Int8) : Int8 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
|
||||
@[extern "lean_int8_xor"]
|
||||
def Int8.xor (a b : Int8) : Int8 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
|
||||
@[extern "lean_int8_shift_left"]
|
||||
def Int8.shiftLeft (a b : Int8) : Int8 := ⟨⟨a.toBitVec <<< (mod b 8).toBitVec⟩⟩
|
||||
def Int8.shiftLeft (a b : Int8) : Int8 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 8)⟩⟩
|
||||
@[extern "lean_int8_shift_right"]
|
||||
def Int8.shiftRight (a b : Int8) : Int8 := ⟨⟨BitVec.sshiftRight' a.toBitVec (mod b 8).toBitVec⟩⟩
|
||||
def Int8.shiftRight (a b : Int8) : Int8 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 8)⟩⟩
|
||||
@[extern "lean_int8_complement"]
|
||||
def Int8.complement (a : Int8) : Int8 := ⟨⟨~~~a.toBitVec⟩⟩
|
||||
|
||||
@@ -114,3 +148,318 @@ instance (a b : Int8) : Decidable (a < b) := Int8.decLt a b
|
||||
instance (a b : Int8) : Decidable (a ≤ b) := Int8.decLe a b
|
||||
instance : Max Int8 := maxOfLe
|
||||
instance : Min Int8 := minOfLe
|
||||
|
||||
/-- The size of type `Int16`, that is, `2^16 = 65536`. -/
|
||||
abbrev Int16.size : Nat := 65536
|
||||
|
||||
/--
|
||||
Obtain the `BitVec` that contains the 2's complement representation of the `Int16`.
|
||||
-/
|
||||
@[inline] def Int16.toBitVec (x : Int16) : BitVec 16 := x.toUInt16.toBitVec
|
||||
|
||||
@[extern "lean_int16_of_int"]
|
||||
def Int16.ofInt (i : @& Int) : Int16 := ⟨⟨BitVec.ofInt 16 i⟩⟩
|
||||
@[extern "lean_int16_of_nat"]
|
||||
def Int16.ofNat (n : @& Nat) : Int16 := ⟨⟨BitVec.ofNat 16 n⟩⟩
|
||||
abbrev Int.toInt16 := Int16.ofInt
|
||||
abbrev Nat.toInt16 := Int16.ofNat
|
||||
@[extern "lean_int16_to_int"]
|
||||
def Int16.toInt (i : Int16) : Int := i.toBitVec.toInt
|
||||
/--
|
||||
This function has the same behavior as `Int.toNat` for negative numbers.
|
||||
If you want to obtain the 2's complement representation use `toBitVec`.
|
||||
-/
|
||||
@[inline] def Int16.toNat (i : Int16) : Nat := i.toInt.toNat
|
||||
@[extern "lean_int16_to_int8"]
|
||||
def Int16.toInt8 (a : Int16) : Int8 := ⟨⟨a.toBitVec.signExtend 8⟩⟩
|
||||
@[extern "lean_int8_to_int16"]
|
||||
def Int8.toInt16 (a : Int8) : Int16 := ⟨⟨a.toBitVec.signExtend 16⟩⟩
|
||||
@[extern "lean_int16_neg"]
|
||||
def Int16.neg (i : Int16) : Int16 := ⟨⟨-i.toBitVec⟩⟩
|
||||
|
||||
instance : ToString Int16 where
|
||||
toString i := toString i.toInt
|
||||
|
||||
instance : OfNat Int16 n := ⟨Int16.ofNat n⟩
|
||||
instance : Neg Int16 where
|
||||
neg := Int16.neg
|
||||
|
||||
@[extern "lean_int16_add"]
|
||||
def Int16.add (a b : Int16) : Int16 := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
|
||||
@[extern "lean_int16_sub"]
|
||||
def Int16.sub (a b : Int16) : Int16 := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
|
||||
@[extern "lean_int16_mul"]
|
||||
def Int16.mul (a b : Int16) : Int16 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
|
||||
@[extern "lean_int16_div"]
|
||||
def Int16.div (a b : Int16) : Int16 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
|
||||
@[extern "lean_int16_mod"]
|
||||
def Int16.mod (a b : Int16) : Int16 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
|
||||
@[extern "lean_int16_land"]
|
||||
def Int16.land (a b : Int16) : Int16 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
|
||||
@[extern "lean_int16_lor"]
|
||||
def Int16.lor (a b : Int16) : Int16 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
|
||||
@[extern "lean_int16_xor"]
|
||||
def Int16.xor (a b : Int16) : Int16 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
|
||||
@[extern "lean_int16_shift_left"]
|
||||
def Int16.shiftLeft (a b : Int16) : Int16 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 16)⟩⟩
|
||||
@[extern "lean_int16_shift_right"]
|
||||
def Int16.shiftRight (a b : Int16) : Int16 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 16)⟩⟩
|
||||
@[extern "lean_int16_complement"]
|
||||
def Int16.complement (a : Int16) : Int16 := ⟨⟨~~~a.toBitVec⟩⟩
|
||||
|
||||
@[extern "lean_int16_dec_eq"]
|
||||
def Int16.decEq (a b : Int16) : Decidable (a = b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ =>
|
||||
if h : n = m then
|
||||
isTrue <| h ▸ rfl
|
||||
else
|
||||
isFalse (fun h' => Int16.noConfusion h' (fun h' => absurd h' h))
|
||||
|
||||
def Int16.lt (a b : Int16) : Prop := a.toBitVec.slt b.toBitVec
|
||||
def Int16.le (a b : Int16) : Prop := a.toBitVec.sle b.toBitVec
|
||||
|
||||
instance : Inhabited Int16 where
|
||||
default := 0
|
||||
|
||||
instance : Add Int16 := ⟨Int16.add⟩
|
||||
instance : Sub Int16 := ⟨Int16.sub⟩
|
||||
instance : Mul Int16 := ⟨Int16.mul⟩
|
||||
instance : Mod Int16 := ⟨Int16.mod⟩
|
||||
instance : Div Int16 := ⟨Int16.div⟩
|
||||
instance : LT Int16 := ⟨Int16.lt⟩
|
||||
instance : LE Int16 := ⟨Int16.le⟩
|
||||
instance : Complement Int16 := ⟨Int16.complement⟩
|
||||
instance : AndOp Int16 := ⟨Int16.land⟩
|
||||
instance : OrOp Int16 := ⟨Int16.lor⟩
|
||||
instance : Xor Int16 := ⟨Int16.xor⟩
|
||||
instance : ShiftLeft Int16 := ⟨Int16.shiftLeft⟩
|
||||
instance : ShiftRight Int16 := ⟨Int16.shiftRight⟩
|
||||
instance : DecidableEq Int16 := Int16.decEq
|
||||
|
||||
@[extern "lean_int16_dec_lt"]
|
||||
def Int16.decLt (a b : Int16) : Decidable (a < b) :=
|
||||
inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
|
||||
|
||||
@[extern "lean_int16_dec_le"]
|
||||
def Int16.decLe (a b : Int16) : Decidable (a ≤ b) :=
|
||||
inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
|
||||
|
||||
instance (a b : Int16) : Decidable (a < b) := Int16.decLt a b
|
||||
instance (a b : Int16) : Decidable (a ≤ b) := Int16.decLe a b
|
||||
instance : Max Int16 := maxOfLe
|
||||
instance : Min Int16 := minOfLe
|
||||
|
||||
/-- The size of type `Int32`, that is, `2^32 = 4294967296`. -/
|
||||
abbrev Int32.size : Nat := 4294967296
|
||||
|
||||
/--
|
||||
Obtain the `BitVec` that contains the 2's complement representation of the `Int32`.
|
||||
-/
|
||||
@[inline] def Int32.toBitVec (x : Int32) : BitVec 32 := x.toUInt32.toBitVec
|
||||
|
||||
@[extern "lean_int32_of_int"]
|
||||
def Int32.ofInt (i : @& Int) : Int32 := ⟨⟨BitVec.ofInt 32 i⟩⟩
|
||||
@[extern "lean_int32_of_nat"]
|
||||
def Int32.ofNat (n : @& Nat) : Int32 := ⟨⟨BitVec.ofNat 32 n⟩⟩
|
||||
abbrev Int.toInt32 := Int32.ofInt
|
||||
abbrev Nat.toInt32 := Int32.ofNat
|
||||
@[extern "lean_int32_to_int"]
|
||||
def Int32.toInt (i : Int32) : Int := i.toBitVec.toInt
|
||||
/--
|
||||
This function has the same behavior as `Int.toNat` for negative numbers.
|
||||
If you want to obtain the 2's complement representation use `toBitVec`.
|
||||
-/
|
||||
@[inline] def Int32.toNat (i : Int32) : Nat := i.toInt.toNat
|
||||
@[extern "lean_int32_to_int8"]
|
||||
def Int32.toInt8 (a : Int32) : Int8 := ⟨⟨a.toBitVec.signExtend 8⟩⟩
|
||||
@[extern "lean_int32_to_int16"]
|
||||
def Int32.toInt16 (a : Int32) : Int16 := ⟨⟨a.toBitVec.signExtend 16⟩⟩
|
||||
@[extern "lean_int8_to_int32"]
|
||||
def Int8.toInt32 (a : Int8) : Int32 := ⟨⟨a.toBitVec.signExtend 32⟩⟩
|
||||
@[extern "lean_int16_to_int32"]
|
||||
def Int16.toInt32 (a : Int16) : Int32 := ⟨⟨a.toBitVec.signExtend 32⟩⟩
|
||||
@[extern "lean_int32_neg"]
|
||||
def Int32.neg (i : Int32) : Int32 := ⟨⟨-i.toBitVec⟩⟩
|
||||
|
||||
instance : ToString Int32 where
|
||||
toString i := toString i.toInt
|
||||
|
||||
instance : OfNat Int32 n := ⟨Int32.ofNat n⟩
|
||||
instance : Neg Int32 where
|
||||
neg := Int32.neg
|
||||
|
||||
@[extern "lean_int32_add"]
|
||||
def Int32.add (a b : Int32) : Int32 := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
|
||||
@[extern "lean_int32_sub"]
|
||||
def Int32.sub (a b : Int32) : Int32 := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
|
||||
@[extern "lean_int32_mul"]
|
||||
def Int32.mul (a b : Int32) : Int32 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
|
||||
@[extern "lean_int32_div"]
|
||||
def Int32.div (a b : Int32) : Int32 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
|
||||
@[extern "lean_int32_mod"]
|
||||
def Int32.mod (a b : Int32) : Int32 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
|
||||
@[extern "lean_int32_land"]
|
||||
def Int32.land (a b : Int32) : Int32 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
|
||||
@[extern "lean_int32_lor"]
|
||||
def Int32.lor (a b : Int32) : Int32 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
|
||||
@[extern "lean_int32_xor"]
|
||||
def Int32.xor (a b : Int32) : Int32 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
|
||||
@[extern "lean_int32_shift_left"]
|
||||
def Int32.shiftLeft (a b : Int32) : Int32 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 32)⟩⟩
|
||||
@[extern "lean_int32_shift_right"]
|
||||
def Int32.shiftRight (a b : Int32) : Int32 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 32)⟩⟩
|
||||
@[extern "lean_int32_complement"]
|
||||
def Int32.complement (a : Int32) : Int32 := ⟨⟨~~~a.toBitVec⟩⟩
|
||||
|
||||
@[extern "lean_int32_dec_eq"]
|
||||
def Int32.decEq (a b : Int32) : Decidable (a = b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ =>
|
||||
if h : n = m then
|
||||
isTrue <| h ▸ rfl
|
||||
else
|
||||
isFalse (fun h' => Int32.noConfusion h' (fun h' => absurd h' h))
|
||||
|
||||
def Int32.lt (a b : Int32) : Prop := a.toBitVec.slt b.toBitVec
|
||||
def Int32.le (a b : Int32) : Prop := a.toBitVec.sle b.toBitVec
|
||||
|
||||
instance : Inhabited Int32 where
|
||||
default := 0
|
||||
|
||||
instance : Add Int32 := ⟨Int32.add⟩
|
||||
instance : Sub Int32 := ⟨Int32.sub⟩
|
||||
instance : Mul Int32 := ⟨Int32.mul⟩
|
||||
instance : Mod Int32 := ⟨Int32.mod⟩
|
||||
instance : Div Int32 := ⟨Int32.div⟩
|
||||
instance : LT Int32 := ⟨Int32.lt⟩
|
||||
instance : LE Int32 := ⟨Int32.le⟩
|
||||
instance : Complement Int32 := ⟨Int32.complement⟩
|
||||
instance : AndOp Int32 := ⟨Int32.land⟩
|
||||
instance : OrOp Int32 := ⟨Int32.lor⟩
|
||||
instance : Xor Int32 := ⟨Int32.xor⟩
|
||||
instance : ShiftLeft Int32 := ⟨Int32.shiftLeft⟩
|
||||
instance : ShiftRight Int32 := ⟨Int32.shiftRight⟩
|
||||
instance : DecidableEq Int32 := Int32.decEq
|
||||
|
||||
@[extern "lean_int32_dec_lt"]
|
||||
def Int32.decLt (a b : Int32) : Decidable (a < b) :=
|
||||
inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
|
||||
|
||||
@[extern "lean_int32_dec_le"]
|
||||
def Int32.decLe (a b : Int32) : Decidable (a ≤ b) :=
|
||||
inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
|
||||
|
||||
instance (a b : Int32) : Decidable (a < b) := Int32.decLt a b
|
||||
instance (a b : Int32) : Decidable (a ≤ b) := Int32.decLe a b
|
||||
instance : Max Int32 := maxOfLe
|
||||
instance : Min Int32 := minOfLe
|
||||
|
||||
/-- The size of type `Int64`, that is, `2^64 = 18446744073709551616`. -/
|
||||
abbrev Int64.size : Nat := 18446744073709551616
|
||||
|
||||
/--
|
||||
Obtain the `BitVec` that contains the 2's complement representation of the `Int64`.
|
||||
-/
|
||||
@[inline] def Int64.toBitVec (x : Int64) : BitVec 64 := x.toUInt64.toBitVec
|
||||
|
||||
@[extern "lean_int64_of_int"]
|
||||
def Int64.ofInt (i : @& Int) : Int64 := ⟨⟨BitVec.ofInt 64 i⟩⟩
|
||||
@[extern "lean_int64_of_nat"]
|
||||
def Int64.ofNat (n : @& Nat) : Int64 := ⟨⟨BitVec.ofNat 64 n⟩⟩
|
||||
abbrev Int.toInt64 := Int64.ofInt
|
||||
abbrev Nat.toInt64 := Int64.ofNat
|
||||
@[extern "lean_int64_to_int_sint"]
|
||||
def Int64.toInt (i : Int64) : Int := i.toBitVec.toInt
|
||||
/--
|
||||
This function has the same behavior as `Int.toNat` for negative numbers.
|
||||
If you want to obtain the 2's complement representation use `toBitVec`.
|
||||
-/
|
||||
@[inline] def Int64.toNat (i : Int64) : Nat := i.toInt.toNat
|
||||
@[extern "lean_int64_to_int8"]
|
||||
def Int64.toInt8 (a : Int64) : Int8 := ⟨⟨a.toBitVec.signExtend 8⟩⟩
|
||||
@[extern "lean_int64_to_int16"]
|
||||
def Int64.toInt16 (a : Int64) : Int16 := ⟨⟨a.toBitVec.signExtend 16⟩⟩
|
||||
@[extern "lean_int64_to_int32"]
|
||||
def Int64.toInt32 (a : Int64) : Int32 := ⟨⟨a.toBitVec.signExtend 32⟩⟩
|
||||
@[extern "lean_int8_to_int64"]
|
||||
def Int8.toInt64 (a : Int8) : Int64 := ⟨⟨a.toBitVec.signExtend 64⟩⟩
|
||||
@[extern "lean_int16_to_int64"]
|
||||
def Int16.toInt64 (a : Int16) : Int64 := ⟨⟨a.toBitVec.signExtend 64⟩⟩
|
||||
@[extern "lean_int32_to_int64"]
|
||||
def Int32.toInt64 (a : Int32) : Int64 := ⟨⟨a.toBitVec.signExtend 64⟩⟩
|
||||
@[extern "lean_int64_neg"]
|
||||
def Int64.neg (i : Int64) : Int64 := ⟨⟨-i.toBitVec⟩⟩
|
||||
|
||||
instance : ToString Int64 where
|
||||
toString i := toString i.toInt
|
||||
|
||||
instance : OfNat Int64 n := ⟨Int64.ofNat n⟩
|
||||
instance : Neg Int64 where
|
||||
neg := Int64.neg
|
||||
|
||||
@[extern "lean_int64_add"]
|
||||
def Int64.add (a b : Int64) : Int64 := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
|
||||
@[extern "lean_int64_sub"]
|
||||
def Int64.sub (a b : Int64) : Int64 := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
|
||||
@[extern "lean_int64_mul"]
|
||||
def Int64.mul (a b : Int64) : Int64 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
|
||||
@[extern "lean_int64_div"]
|
||||
def Int64.div (a b : Int64) : Int64 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
|
||||
@[extern "lean_int64_mod"]
|
||||
def Int64.mod (a b : Int64) : Int64 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
|
||||
@[extern "lean_int64_land"]
|
||||
def Int64.land (a b : Int64) : Int64 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
|
||||
@[extern "lean_int64_lor"]
|
||||
def Int64.lor (a b : Int64) : Int64 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
|
||||
@[extern "lean_int64_xor"]
|
||||
def Int64.xor (a b : Int64) : Int64 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
|
||||
@[extern "lean_int64_shift_left"]
|
||||
def Int64.shiftLeft (a b : Int64) : Int64 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 64)⟩⟩
|
||||
@[extern "lean_int64_shift_right"]
|
||||
def Int64.shiftRight (a b : Int64) : Int64 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 64)⟩⟩
|
||||
@[extern "lean_int64_complement"]
|
||||
def Int64.complement (a : Int64) : Int64 := ⟨⟨~~~a.toBitVec⟩⟩
|
||||
|
||||
@[extern "lean_int64_dec_eq"]
|
||||
def Int64.decEq (a b : Int64) : Decidable (a = b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ =>
|
||||
if h : n = m then
|
||||
isTrue <| h ▸ rfl
|
||||
else
|
||||
isFalse (fun h' => Int64.noConfusion h' (fun h' => absurd h' h))
|
||||
|
||||
def Int64.lt (a b : Int64) : Prop := a.toBitVec.slt b.toBitVec
|
||||
def Int64.le (a b : Int64) : Prop := a.toBitVec.sle b.toBitVec
|
||||
|
||||
instance : Inhabited Int64 where
|
||||
default := 0
|
||||
|
||||
instance : Add Int64 := ⟨Int64.add⟩
|
||||
instance : Sub Int64 := ⟨Int64.sub⟩
|
||||
instance : Mul Int64 := ⟨Int64.mul⟩
|
||||
instance : Mod Int64 := ⟨Int64.mod⟩
|
||||
instance : Div Int64 := ⟨Int64.div⟩
|
||||
instance : LT Int64 := ⟨Int64.lt⟩
|
||||
instance : LE Int64 := ⟨Int64.le⟩
|
||||
instance : Complement Int64 := ⟨Int64.complement⟩
|
||||
instance : AndOp Int64 := ⟨Int64.land⟩
|
||||
instance : OrOp Int64 := ⟨Int64.lor⟩
|
||||
instance : Xor Int64 := ⟨Int64.xor⟩
|
||||
instance : ShiftLeft Int64 := ⟨Int64.shiftLeft⟩
|
||||
instance : ShiftRight Int64 := ⟨Int64.shiftRight⟩
|
||||
instance : DecidableEq Int64 := Int64.decEq
|
||||
|
||||
@[extern "lean_int64_dec_lt"]
|
||||
def Int64.decLt (a b : Int64) : Decidable (a < b) :=
|
||||
inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
|
||||
|
||||
@[extern "lean_int64_dec_le"]
|
||||
def Int64.decLe (a b : Int64) : Decidable (a ≤ b) :=
|
||||
inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
|
||||
|
||||
instance (a b : Int64) : Decidable (a < b) := Int64.decLt a b
|
||||
instance (a b : Int64) : Decidable (a ≤ b) := Int64.decLe a b
|
||||
instance : Max Int64 := maxOfLe
|
||||
instance : Min Int64 := minOfLe
|
||||
|
||||
@@ -211,10 +211,13 @@ instance : GetElem (List α) Nat α fun as i => i < as.length where
|
||||
| _ :: _, 0, _ => .head ..
|
||||
| _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
|
||||
|
||||
theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
|
||||
theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.length) :
|
||||
as[i] :: as.drop (i+1) = as.drop i :=
|
||||
match as, i with
|
||||
| _::_, 0 => rfl
|
||||
| _::_, i+1 => get_drop_eq_drop _ i _
|
||||
| _::_, i+1 => getElem_cons_drop_succ_eq_drop (i := i) _
|
||||
|
||||
@[deprecated (since := "2024-11-05")] abbrev get_drop_eq_drop := @getElem_cons_drop_succ_eq_drop
|
||||
|
||||
end List
|
||||
|
||||
|
||||
@@ -272,12 +272,20 @@ macro nextTk:"next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
|
||||
-- Limit ref variability for incrementality; see Note [Incremental Macros]
|
||||
withRef arrowTk `(tactic| case%$nextTk _ $args* =>%$arrowTk $tac)
|
||||
|
||||
/-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
|
||||
/--
|
||||
`all_goals tac` runs `tac` on each goal, concatenating the resulting goals.
|
||||
If the tactic fails on any goal, the entire `all_goals` tactic fails.
|
||||
|
||||
See also `any_goals tac`.
|
||||
-/
|
||||
syntax (name := allGoals) "all_goals " tacticSeq : tactic
|
||||
|
||||
/--
|
||||
`any_goals tac` applies the tactic `tac` to every goal, and succeeds if at
|
||||
least one application succeeds.
|
||||
`any_goals tac` applies the tactic `tac` to every goal,
|
||||
concating the resulting goals for successful tactic applications.
|
||||
If the tactic fails on all of the goals, the entire `any_goals` tactic fails.
|
||||
|
||||
This tactic is like `all_goals try tac` except that it fails if none of the applications of `tac` succeeds.
|
||||
-/
|
||||
syntax (name := anyGoals) "any_goals " tacticSeq : tactic
|
||||
|
||||
|
||||
@@ -35,9 +35,13 @@ Reconstruct bit by bit which value expression must have had which `BitVec` value
|
||||
expression - pair values.
|
||||
-/
|
||||
def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Array (Bool × Nat))
|
||||
(aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
|
||||
(aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
|
||||
Array (Expr × BVExpr.PackedBitVec) := Id.run do
|
||||
let mut sparseMap : Std.HashMap Nat (RBMap Nat Bool Ord.compare) := {}
|
||||
let filter bvBit _ :=
|
||||
let (_, _, synthetic) := atomsAssignment.get! bvBit.var
|
||||
!synthetic
|
||||
let var2Cnf := var2Cnf.filter filter
|
||||
for (bitVar, cnfVar) in var2Cnf.toArray do
|
||||
/-
|
||||
The setup of the variables in CNF is as follows:
|
||||
@@ -70,7 +74,7 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
|
||||
if bitValue then
|
||||
value := value ||| (1 <<< currentBit)
|
||||
currentBit := currentBit + 1
|
||||
let atomExpr := atomsAssignment.get! bitVecVar |>.snd
|
||||
let (_, atomExpr, _) := atomsAssignment.get! bitVecVar
|
||||
finalMap := finalMap.push (atomExpr, ⟨BitVec.ofNat currentBit value⟩)
|
||||
return finalMap
|
||||
|
||||
@@ -101,7 +105,7 @@ structure UnsatProver.Result where
|
||||
proof : Expr
|
||||
lratCert : LratCert
|
||||
|
||||
abbrev UnsatProver := MVarId → ReflectionResult → Std.HashMap Nat (Nat × Expr) →
|
||||
abbrev UnsatProver := MVarId → ReflectionResult → Std.HashMap Nat (Nat × Expr × Bool) →
|
||||
MetaM (Except CounterExample UnsatProver.Result)
|
||||
|
||||
/--
|
||||
@@ -183,7 +187,7 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa
|
||||
return err
|
||||
|
||||
def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : ReflectionResult)
|
||||
(atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
|
||||
(atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
|
||||
MetaM (Except CounterExample UnsatProver.Result) := do
|
||||
let bvExpr := reflectionResult.bvExpr
|
||||
let entry ←
|
||||
@@ -253,7 +257,8 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
|
||||
reflectBV g
|
||||
trace[Meta.Tactic.bv] "Reflected bv logical expression: {reflectionResult.bvExpr}"
|
||||
|
||||
let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, ⟨width, ident⟩) => (ident, (width, expr)))
|
||||
let flipper := (fun (expr, {width, atomNumber, synthetic}) => (atomNumber, (width, expr, synthetic)))
|
||||
let atomsPairs := (← getThe State).atoms.toList.map flipper
|
||||
let atomsAssignment := Std.HashMap.ofList atomsPairs
|
||||
match ← unsatProver g reflectionResult atomsAssignment with
|
||||
| .ok ⟨bvExprUnsat, cert⟩ =>
|
||||
|
||||
@@ -107,6 +107,25 @@ where
|
||||
|
||||
open Lean.Meta
|
||||
|
||||
/--
|
||||
A `BitVec` atom.
|
||||
-/
|
||||
structure Atom where
|
||||
/--
|
||||
The width of the `BitVec` that is being abstracted.
|
||||
-/
|
||||
width : Nat
|
||||
/--
|
||||
A unique numeric identifier for the atom.
|
||||
-/
|
||||
atomNumber : Nat
|
||||
/--
|
||||
Whether the atom is synthetic. The effect of this is that values for this atom are not considered
|
||||
for the counter example deriviation. This is for example useful when we introduce an atom over
|
||||
an expression, together with additional lemmas that fully describe the behavior of the atom.
|
||||
-/
|
||||
synthetic : Bool
|
||||
|
||||
/--
|
||||
The state of the reflection monad
|
||||
-/
|
||||
@@ -115,7 +134,7 @@ structure State where
|
||||
The atoms encountered so far. Saved as a map from `BitVec` expressions to a (width, atomNumber)
|
||||
pair.
|
||||
-/
|
||||
atoms : Std.HashMap Expr (Nat × Nat) := {}
|
||||
atoms : Std.HashMap Expr Atom := {}
|
||||
/--
|
||||
A cache for `atomsAssignment`.
|
||||
-/
|
||||
@@ -208,8 +227,8 @@ def run (m : M α) : MetaM α :=
|
||||
Retrieve the atoms as pairs of their width and expression.
|
||||
-/
|
||||
def atoms : M (List (Nat × Expr)) := do
|
||||
let sortedAtoms := (← getThe State).atoms.toArray.qsort (·.2.2 < ·.2.2)
|
||||
return sortedAtoms.map (fun (expr, width, _) => (width, expr)) |>.toList
|
||||
let sortedAtoms := (← getThe State).atoms.toArray.qsort (·.2.atomNumber < ·.2.atomNumber)
|
||||
return sortedAtoms.map (fun (expr, {width, ..}) => (width, expr)) |>.toList
|
||||
|
||||
/--
|
||||
Retrieve a `BitVec.Assignment` representing the atoms we found so far.
|
||||
@@ -220,16 +239,17 @@ def atomsAssignment : M Expr := do
|
||||
/--
|
||||
Look up an expression in the atoms, recording it if it has not previously appeared.
|
||||
-/
|
||||
def lookup (e : Expr) (width : Nat) : M Nat := do
|
||||
def lookup (e : Expr) (width : Nat) (synthetic : Bool) : M Nat := do
|
||||
match (← getThe State).atoms[e]? with
|
||||
| some (width', ident) =>
|
||||
if width != width' then
|
||||
| some atom =>
|
||||
if width != atom.width then
|
||||
panic! "The same atom occurs with different widths, this is a bug"
|
||||
return ident
|
||||
return atom.atomNumber
|
||||
| none =>
|
||||
trace[Meta.Tactic.bv] "New atom of width {width}: {e}"
|
||||
trace[Meta.Tactic.bv] "New atom of width {width}, synthetic? {synthetic}: {e}"
|
||||
let ident ← modifyGetThe State fun s =>
|
||||
(s.atoms.size, { s with atoms := s.atoms.insert e (width, s.atoms.size) })
|
||||
let newAtom := { width, synthetic, atomNumber := s.atoms.size}
|
||||
(s.atoms.size, { s with atoms := s.atoms.insert e newAtom })
|
||||
updateAtomsAssignment
|
||||
return ident
|
||||
where
|
||||
|
||||
@@ -32,10 +32,10 @@ def mkBVRefl (w : Nat) (expr : Expr) : Expr :=
|
||||
expr
|
||||
|
||||
/--
|
||||
Register `e` as an atom of width `width`.
|
||||
Register `e` as an atom of `width` that might potentially be `synthetic`.
|
||||
-/
|
||||
def mkAtom (e : Expr) (width : Nat) : M ReifiedBVExpr := do
|
||||
let ident ← M.lookup e width
|
||||
def mkAtom (e : Expr) (width : Nat) (synthetic : Bool) : M ReifiedBVExpr := do
|
||||
let ident ← M.lookup e width synthetic
|
||||
let expr := mkApp2 (mkConst ``BVExpr.var) (toExpr width) (toExpr ident)
|
||||
let proof := do
|
||||
let evalExpr ← mkEvalExpr width expr
|
||||
@@ -55,13 +55,13 @@ def getNatOrBvValue? (ty : Expr) (expr : Expr) : M (Option Nat) := do
|
||||
| _ => return none
|
||||
|
||||
/--
|
||||
Construct an uninterpreted `BitVec` atom from `x`.
|
||||
Construct an uninterpreted `BitVec` atom from `x`, potentially `synthetic`.
|
||||
-/
|
||||
def bitVecAtom (x : Expr) : M (Option ReifiedBVExpr) := do
|
||||
def bitVecAtom (x : Expr) (synthetic : Bool) : M (Option ReifiedBVExpr) := do
|
||||
let t ← instantiateMVars (← whnfR (← inferType x))
|
||||
let_expr BitVec widthExpr := t | return none
|
||||
let some width ← getNatValue? widthExpr | return none
|
||||
let atom ← mkAtom x width
|
||||
let atom ← mkAtom x width synthetic
|
||||
return some atom
|
||||
|
||||
/--
|
||||
|
||||
@@ -31,7 +31,7 @@ def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
|
||||
-/
|
||||
let ty ← inferType t
|
||||
let_expr Bool := ty | return none
|
||||
let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1
|
||||
let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1 false
|
||||
let bvExpr : BVPred := .getLsbD atom.bvExpr 0
|
||||
let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
|
||||
let proof := do
|
||||
|
||||
@@ -209,7 +209,7 @@ where
|
||||
let_expr Eq α discrExpr val := discrExpr | return none
|
||||
let_expr Bool := α | return none
|
||||
let_expr Bool.true := val | return none
|
||||
let some atom ← ReifiedBVExpr.bitVecAtom x | return none
|
||||
let some atom ← ReifiedBVExpr.bitVecAtom x true | return none
|
||||
let some discr ← ReifiedBVLogical.of discrExpr | return none
|
||||
let some lhs ← goOrAtom lhsExpr | return none
|
||||
let some rhs ← goOrAtom rhsExpr | return none
|
||||
@@ -226,7 +226,7 @@ where
|
||||
let res ← go x
|
||||
match res with
|
||||
| some exp => return some exp
|
||||
| none => ReifiedBVExpr.bitVecAtom x
|
||||
| none => ReifiedBVExpr.bitVecAtom x false
|
||||
|
||||
shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
|
||||
(shiftOpName : Name) (congrThm : Name) :
|
||||
@@ -316,7 +316,7 @@ where
|
||||
return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof
|
||||
|
||||
goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do
|
||||
let some ⟨_, bvVal⟩ ← getBitVecValue? x | return ← ReifiedBVExpr.bitVecAtom x
|
||||
let some ⟨_, bvVal⟩ ← getBitVecValue? x | return ← ReifiedBVExpr.bitVecAtom x false
|
||||
ReifiedBVExpr.mkBVConst bvVal
|
||||
|
||||
/--
|
||||
|
||||
@@ -263,19 +263,26 @@ private def getOptRotation (stx : Syntax) : Nat :=
|
||||
@[builtin_tactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do
|
||||
let mvarIds ← getGoals
|
||||
let mut mvarIdsNew := #[]
|
||||
let mut abort := false
|
||||
let mut mctxSaved ← getMCtx
|
||||
for mvarId in mvarIds do
|
||||
unless (← mvarId.isAssigned) do
|
||||
setGoals [mvarId]
|
||||
mvarIdsNew ← Tactic.tryCatch
|
||||
abort ← Tactic.tryCatch
|
||||
(do
|
||||
evalTactic stx[1]
|
||||
return mvarIdsNew ++ (← getUnsolvedGoals))
|
||||
pure abort)
|
||||
(fun ex => do
|
||||
if (← read).recover then
|
||||
logException ex
|
||||
return mvarIdsNew.push mvarId
|
||||
pure true
|
||||
else
|
||||
throw ex)
|
||||
mvarIdsNew := mvarIdsNew ++ (← getUnsolvedGoals)
|
||||
if abort then
|
||||
setMCtx mctxSaved
|
||||
mvarIds.forM fun mvarId => unless (← mvarId.isAssigned) do admitGoal mvarId
|
||||
throwAbortTactic
|
||||
setGoals mvarIdsNew.toList
|
||||
|
||||
@[builtin_tactic Parser.Tactic.anyGoals] def evalAnyGoals : Tactic := fun stx => do
|
||||
|
||||
@@ -1651,7 +1651,7 @@ static inline uint8_t lean_uint8_dec_lt(uint8_t a1, uint8_t a2) { return a1 < a2
|
||||
static inline uint8_t lean_uint8_dec_le(uint8_t a1, uint8_t a2) { return a1 <= a2; }
|
||||
|
||||
|
||||
/* Unit8 -> other */
|
||||
/* UInt8 -> other */
|
||||
static inline uint16_t lean_uint8_to_uint16(uint8_t a) { return ((uint16_t)a); }
|
||||
static inline uint32_t lean_uint8_to_uint32(uint8_t a) { return ((uint32_t)a); }
|
||||
static inline uint64_t lean_uint8_to_uint64(uint8_t a) { return ((uint64_t)a); }
|
||||
@@ -1686,7 +1686,7 @@ static inline uint8_t lean_uint16_dec_eq(uint16_t a1, uint16_t a2) { return a1 =
|
||||
static inline uint8_t lean_uint16_dec_lt(uint16_t a1, uint16_t a2) { return a1 < a2; }
|
||||
static inline uint8_t lean_uint16_dec_le(uint16_t a1, uint16_t a2) { return a1 <= a2; }
|
||||
|
||||
/*uint16 -> other */
|
||||
/* UInt16 -> other */
|
||||
static inline uint8_t lean_uint16_to_uint8(uint16_t a) { return ((uint8_t)a); }
|
||||
static inline uint32_t lean_uint16_to_uint32(uint16_t a) { return ((uint32_t)a); }
|
||||
static inline uint64_t lean_uint16_to_uint64(uint16_t a) { return ((uint64_t)a); }
|
||||
@@ -1721,7 +1721,7 @@ static inline uint8_t lean_uint32_dec_eq(uint32_t a1, uint32_t a2) { return a1 =
|
||||
static inline uint8_t lean_uint32_dec_lt(uint32_t a1, uint32_t a2) { return a1 < a2; }
|
||||
static inline uint8_t lean_uint32_dec_le(uint32_t a1, uint32_t a2) { return a1 <= a2; }
|
||||
|
||||
/* uint32 -> other */
|
||||
/* UInt32 -> other */
|
||||
static inline uint8_t lean_uint32_to_uint8(uint32_t a) { return ((uint8_t)a); }
|
||||
static inline uint16_t lean_uint32_to_uint16(uint32_t a) { return ((uint16_t)a); }
|
||||
static inline uint64_t lean_uint32_to_uint64(uint32_t a) { return ((uint64_t)a); }
|
||||
@@ -1759,7 +1759,7 @@ static inline uint8_t lean_uint64_dec_le(uint64_t a1, uint64_t a2) { return a1 <
|
||||
LEAN_EXPORT uint64_t lean_uint64_mix_hash(uint64_t a1, uint64_t a2);
|
||||
|
||||
|
||||
/* uint64 -> other */
|
||||
/* UInt64 -> other */
|
||||
static inline uint8_t lean_uint64_to_uint8(uint64_t a) { return ((uint8_t)a); }
|
||||
static inline uint16_t lean_uint64_to_uint16(uint64_t a) { return ((uint16_t)a); }
|
||||
static inline uint32_t lean_uint64_to_uint32(uint64_t a) { return ((uint32_t)a); }
|
||||
@@ -1826,6 +1826,18 @@ static inline uint8_t lean_int8_of_int(b_lean_obj_arg a) {
|
||||
return (uint8_t)res;
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_of_nat(b_lean_obj_arg a) {
|
||||
int8_t res;
|
||||
|
||||
if (lean_is_scalar(a)) {
|
||||
res = (int8_t)lean_unbox(a);
|
||||
} else {
|
||||
res = lean_int8_of_big_int(a);
|
||||
}
|
||||
|
||||
return (uint8_t)res;
|
||||
}
|
||||
|
||||
static inline lean_obj_res lean_int8_to_int(uint8_t a) {
|
||||
int8_t arg = (int8_t)a;
|
||||
return lean_int64_to_int((int64_t)arg);
|
||||
@@ -1838,73 +1850,73 @@ static inline uint8_t lean_int8_neg(uint8_t a) {
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_add(uint8_t a1, uint8_t a2) {
|
||||
int8_t lhs = (int8_t) a1;
|
||||
int8_t rhs = (int8_t) a2;
|
||||
int8_t lhs = (int8_t)a1;
|
||||
int8_t rhs = (int8_t)a2;
|
||||
|
||||
return (uint8_t)(lhs + rhs);
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_sub(uint8_t a1, uint8_t a2) {
|
||||
int8_t lhs = (int8_t) a1;
|
||||
int8_t rhs = (int8_t) a2;
|
||||
int8_t lhs = (int8_t)a1;
|
||||
int8_t rhs = (int8_t)a2;
|
||||
|
||||
return (uint8_t)(lhs - rhs);
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_mul(uint8_t a1, uint8_t a2) {
|
||||
int8_t lhs = (int8_t) a1;
|
||||
int8_t rhs = (int8_t) a2;
|
||||
int8_t lhs = (int8_t)a1;
|
||||
int8_t rhs = (int8_t)a2;
|
||||
|
||||
return (uint8_t)(lhs * rhs);
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_div(uint8_t a1, uint8_t a2) {
|
||||
int8_t lhs = (int8_t) a1;
|
||||
int8_t rhs = (int8_t) a2;
|
||||
int8_t lhs = (int8_t)a1;
|
||||
int8_t rhs = (int8_t)a2;
|
||||
|
||||
return (uint8_t)(rhs == 0 ? 0 : lhs / rhs);
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_mod(uint8_t a1, uint8_t a2) {
|
||||
int8_t lhs = (int8_t) a1;
|
||||
int8_t rhs = (int8_t) a2;
|
||||
int8_t lhs = (int8_t)a1;
|
||||
int8_t rhs = (int8_t)a2;
|
||||
|
||||
return (uint8_t)(rhs == 0 ? 0 : lhs % rhs);
|
||||
return (uint8_t)(rhs == 0 ? lhs : lhs % rhs);
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_land(uint8_t a1, uint8_t a2) {
|
||||
int8_t lhs = (int8_t) a1;
|
||||
int8_t rhs = (int8_t) a2;
|
||||
int8_t lhs = (int8_t)a1;
|
||||
int8_t rhs = (int8_t)a2;
|
||||
|
||||
return (uint8_t)(lhs & rhs);
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_lor(uint8_t a1, uint8_t a2) {
|
||||
int8_t lhs = (int8_t) a1;
|
||||
int8_t rhs = (int8_t) a2;
|
||||
int8_t lhs = (int8_t)a1;
|
||||
int8_t rhs = (int8_t)a2;
|
||||
|
||||
return (uint8_t)(lhs | rhs);
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_xor(uint8_t a1, uint8_t a2) {
|
||||
int8_t lhs = (int8_t) a1;
|
||||
int8_t rhs = (int8_t) a2;
|
||||
int8_t lhs = (int8_t)a1;
|
||||
int8_t rhs = (int8_t)a2;
|
||||
|
||||
return (uint8_t)(lhs ^ rhs);
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_shift_right(uint8_t a1, uint8_t a2) {
|
||||
int8_t lhs = (int8_t) a1;
|
||||
int8_t rhs = (int8_t) a2;
|
||||
int8_t lhs = (int8_t)a1;
|
||||
int8_t rhs = (((int8_t)a2 % 8) + 8) % 8; // this is smod 8
|
||||
|
||||
return (uint8_t)(lhs >> (rhs % 8));
|
||||
return (uint8_t)(lhs >> rhs);
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_shift_left(uint8_t a1, uint8_t a2) {
|
||||
int8_t lhs = (int8_t) a1;
|
||||
int8_t rhs = (int8_t) a2;
|
||||
int8_t lhs = (int8_t)a1;
|
||||
int8_t rhs = (((int8_t)a2 % 8) + 8) % 8; // this is smod 8
|
||||
|
||||
return (uint8_t)(lhs << (rhs % 8));
|
||||
return (uint8_t)(lhs << rhs);
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_complement(uint8_t a) {
|
||||
@@ -1914,26 +1926,449 @@ static inline uint8_t lean_int8_complement(uint8_t a) {
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_dec_eq(uint8_t a1, uint8_t a2) {
|
||||
int8_t lhs = (int8_t) a1;
|
||||
int8_t rhs = (int8_t) a2;
|
||||
int8_t lhs = (int8_t)a1;
|
||||
int8_t rhs = (int8_t)a2;
|
||||
|
||||
return lhs == rhs;
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_dec_lt(uint8_t a1, uint8_t a2) {
|
||||
int8_t lhs = (int8_t) a1;
|
||||
int8_t rhs = (int8_t) a2;
|
||||
int8_t lhs = (int8_t)a1;
|
||||
int8_t rhs = (int8_t)a2;
|
||||
|
||||
return lhs < rhs;
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int8_dec_le(uint8_t a1, uint8_t a2) {
|
||||
int8_t lhs = (int8_t) a1;
|
||||
int8_t rhs = (int8_t) a2;
|
||||
int8_t lhs = (int8_t)a1;
|
||||
int8_t rhs = (int8_t)a2;
|
||||
|
||||
return lhs <= rhs;
|
||||
}
|
||||
|
||||
/* Int8 -> other */
|
||||
static inline uint16_t lean_int8_to_int16(uint8_t a) { return (uint16_t)(int16_t)(int8_t)a; }
|
||||
static inline uint32_t lean_int8_to_int32(uint8_t a) { return (uint32_t)(int32_t)(int8_t)a; }
|
||||
static inline uint64_t lean_int8_to_int64(uint8_t a) { return (uint64_t)(int64_t)(int8_t)a; }
|
||||
|
||||
|
||||
/* Int16 */
|
||||
LEAN_EXPORT int16_t lean_int16_of_big_int(b_lean_obj_arg a);
|
||||
static inline uint16_t lean_int16_of_int(b_lean_obj_arg a) {
|
||||
int16_t res;
|
||||
|
||||
if (lean_is_scalar(a)) {
|
||||
res = (int16_t)lean_scalar_to_int64(a);
|
||||
} else {
|
||||
res = lean_int16_of_big_int(a);
|
||||
}
|
||||
|
||||
return (uint16_t)res;
|
||||
}
|
||||
|
||||
static inline uint16_t lean_int16_of_nat(b_lean_obj_arg a) {
|
||||
int16_t res;
|
||||
|
||||
if (lean_is_scalar(a)) {
|
||||
res = (int16_t)lean_unbox(a);
|
||||
} else {
|
||||
res = lean_int16_of_big_int(a);
|
||||
}
|
||||
|
||||
return (uint16_t)res;
|
||||
}
|
||||
|
||||
static inline lean_obj_res lean_int16_to_int(uint16_t a) {
|
||||
int16_t arg = (int16_t)a;
|
||||
return lean_int64_to_int((int64_t)arg);
|
||||
}
|
||||
|
||||
static inline uint16_t lean_int16_neg(uint16_t a) {
|
||||
int16_t arg = (int16_t)a;
|
||||
|
||||
return (uint16_t)(-arg);
|
||||
}
|
||||
|
||||
static inline uint16_t lean_int16_add(uint16_t a1, uint16_t a2) {
|
||||
int16_t lhs = (int16_t)a1;
|
||||
int16_t rhs = (int16_t)a2;
|
||||
|
||||
return (uint16_t)(lhs + rhs);
|
||||
}
|
||||
|
||||
static inline uint16_t lean_int16_sub(uint16_t a1, uint16_t a2) {
|
||||
int16_t lhs = (int16_t)a1;
|
||||
int16_t rhs = (int16_t)a2;
|
||||
|
||||
return (uint16_t)(lhs - rhs);
|
||||
}
|
||||
|
||||
static inline uint16_t lean_int16_mul(uint16_t a1, uint16_t a2) {
|
||||
int16_t lhs = (int16_t)a1;
|
||||
int16_t rhs = (int16_t)a2;
|
||||
|
||||
return (uint16_t)(lhs * rhs);
|
||||
}
|
||||
|
||||
static inline uint16_t lean_int16_div(uint16_t a1, uint16_t a2) {
|
||||
int16_t lhs = (int16_t)a1;
|
||||
int16_t rhs = (int16_t)a2;
|
||||
|
||||
return (uint16_t)(rhs == 0 ? 0 : lhs / rhs);
|
||||
}
|
||||
|
||||
static inline uint16_t lean_int16_mod(uint16_t a1, uint16_t a2) {
|
||||
int16_t lhs = (int16_t)a1;
|
||||
int16_t rhs = (int16_t)a2;
|
||||
|
||||
return (uint16_t)(rhs == 0 ? lhs : lhs % rhs);
|
||||
}
|
||||
|
||||
static inline uint16_t lean_int16_land(uint16_t a1, uint16_t a2) {
|
||||
int16_t lhs = (int16_t)a1;
|
||||
int16_t rhs = (int16_t)a2;
|
||||
|
||||
return (uint16_t)(lhs & rhs);
|
||||
}
|
||||
|
||||
static inline uint16_t lean_int16_lor(uint16_t a1, uint16_t a2) {
|
||||
int16_t lhs = (int16_t)a1;
|
||||
int16_t rhs = (int16_t)a2;
|
||||
|
||||
return (uint16_t)(lhs | rhs);
|
||||
}
|
||||
|
||||
static inline uint16_t lean_int16_xor(uint16_t a1, uint16_t a2) {
|
||||
int16_t lhs = (int16_t)a1;
|
||||
int16_t rhs = (int16_t)a2;
|
||||
|
||||
return (uint16_t)(lhs ^ rhs);
|
||||
}
|
||||
|
||||
static inline uint16_t lean_int16_shift_right(uint16_t a1, uint16_t a2) {
|
||||
int16_t lhs = (int16_t)a1;
|
||||
int16_t rhs = (((int16_t)a2 % 16) + 16) % 16; // this is smod 16
|
||||
|
||||
return (uint16_t)(lhs >> rhs);
|
||||
}
|
||||
|
||||
static inline uint16_t lean_int16_shift_left(uint16_t a1, uint16_t a2) {
|
||||
int16_t lhs = (int16_t)a1;
|
||||
int16_t rhs = (((int16_t)a2 % 16) + 16) % 16; // this is smod 16
|
||||
|
||||
return (uint16_t)(lhs << rhs);
|
||||
}
|
||||
|
||||
static inline uint16_t lean_int16_complement(uint16_t a) {
|
||||
int16_t arg = (int16_t)a;
|
||||
|
||||
return (uint16_t)(~arg);
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int16_dec_eq(uint16_t a1, uint16_t a2) {
|
||||
int16_t lhs = (int16_t)a1;
|
||||
int16_t rhs = (int16_t)a2;
|
||||
|
||||
return lhs == rhs;
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int16_dec_lt(uint16_t a1, uint16_t a2) {
|
||||
int16_t lhs = (int16_t)a1;
|
||||
int16_t rhs = (int16_t)a2;
|
||||
|
||||
return lhs < rhs;
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int16_dec_le(uint16_t a1, uint16_t a2) {
|
||||
int16_t lhs = (int16_t)a1;
|
||||
int16_t rhs = (int16_t)a2;
|
||||
|
||||
return lhs <= rhs;
|
||||
}
|
||||
|
||||
/* Int16 -> other */
|
||||
static inline uint8_t lean_int16_to_int8(uint16_t a) { return (uint8_t)(int8_t)(int16_t)a; }
|
||||
static inline uint32_t lean_int16_to_int32(uint16_t a) { return (uint32_t)(int32_t)(int16_t)a; }
|
||||
static inline uint64_t lean_int16_to_int64(uint16_t a) { return (uint64_t)(int64_t)(int16_t)a; }
|
||||
|
||||
/* Int32 */
|
||||
LEAN_EXPORT int32_t lean_int32_of_big_int(b_lean_obj_arg a);
|
||||
static inline uint32_t lean_int32_of_int(b_lean_obj_arg a) {
|
||||
int32_t res;
|
||||
|
||||
if (lean_is_scalar(a)) {
|
||||
res = (int32_t)lean_scalar_to_int64(a);
|
||||
} else {
|
||||
res = lean_int32_of_big_int(a);
|
||||
}
|
||||
|
||||
return (uint32_t)res;
|
||||
}
|
||||
|
||||
static inline uint32_t lean_int32_of_nat(b_lean_obj_arg a) {
|
||||
int32_t res;
|
||||
|
||||
if (lean_is_scalar(a)) {
|
||||
res = (int32_t)lean_unbox(a);
|
||||
} else {
|
||||
res = lean_int32_of_big_int(a);
|
||||
}
|
||||
|
||||
return (uint32_t)res;
|
||||
}
|
||||
|
||||
static inline lean_obj_res lean_int32_to_int(uint32_t a) {
|
||||
int32_t arg = (int32_t)a;
|
||||
return lean_int64_to_int((int64_t)arg);
|
||||
}
|
||||
|
||||
static inline uint32_t lean_int32_neg(uint32_t a) {
|
||||
int32_t arg = (int32_t)a;
|
||||
|
||||
return (uint32_t)(-arg);
|
||||
}
|
||||
|
||||
static inline uint32_t lean_int32_add(uint32_t a1, uint32_t a2) {
|
||||
int32_t lhs = (int32_t)a1;
|
||||
int32_t rhs = (int32_t)a2;
|
||||
|
||||
return (uint32_t)(lhs + rhs);
|
||||
}
|
||||
|
||||
static inline uint32_t lean_int32_sub(uint32_t a1, uint32_t a2) {
|
||||
int32_t lhs = (int32_t)a1;
|
||||
int32_t rhs = (int32_t)a2;
|
||||
|
||||
return (uint32_t)(lhs - rhs);
|
||||
}
|
||||
|
||||
static inline uint32_t lean_int32_mul(uint32_t a1, uint32_t a2) {
|
||||
int32_t lhs = (int32_t)a1;
|
||||
int32_t rhs = (int32_t)a2;
|
||||
|
||||
return (uint32_t)(lhs * rhs);
|
||||
}
|
||||
|
||||
static inline uint32_t lean_int32_div(uint32_t a1, uint32_t a2) {
|
||||
int32_t lhs = (int32_t)a1;
|
||||
int32_t rhs = (int32_t)a2;
|
||||
|
||||
return (uint32_t)(rhs == 0 ? 0 : lhs / rhs);
|
||||
}
|
||||
|
||||
static inline uint32_t lean_int32_mod(uint32_t a1, uint32_t a2) {
|
||||
int32_t lhs = (int32_t)a1;
|
||||
int32_t rhs = (int32_t)a2;
|
||||
|
||||
return (uint32_t)(rhs == 0 ? lhs : lhs % rhs);
|
||||
}
|
||||
|
||||
static inline uint32_t lean_int32_land(uint32_t a1, uint32_t a2) {
|
||||
int32_t lhs = (int32_t)a1;
|
||||
int32_t rhs = (int32_t)a2;
|
||||
|
||||
return (uint32_t)(lhs & rhs);
|
||||
}
|
||||
|
||||
static inline uint32_t lean_int32_lor(uint32_t a1, uint32_t a2) {
|
||||
int32_t lhs = (int32_t)a1;
|
||||
int32_t rhs = (int32_t)a2;
|
||||
|
||||
return (uint32_t)(lhs | rhs);
|
||||
}
|
||||
|
||||
static inline uint32_t lean_int32_xor(uint32_t a1, uint32_t a2) {
|
||||
int32_t lhs = (int32_t)a1;
|
||||
int32_t rhs = (int32_t)a2;
|
||||
|
||||
return (uint32_t)(lhs ^ rhs);
|
||||
}
|
||||
|
||||
static inline uint32_t lean_int32_shift_right(uint32_t a1, uint32_t a2) {
|
||||
int32_t lhs = (int32_t)a1;
|
||||
int32_t rhs = (((int32_t)a2 % 32) + 32) % 32; // this is smod 32
|
||||
|
||||
return (uint32_t)(lhs >> rhs);
|
||||
}
|
||||
|
||||
static inline uint32_t lean_int32_shift_left(uint32_t a1, uint32_t a2) {
|
||||
int32_t lhs = (int32_t)a1;
|
||||
int32_t rhs = (((int32_t)a2 % 32) + 32) % 32; // this is smod 32
|
||||
|
||||
return (uint32_t)(lhs << rhs);
|
||||
}
|
||||
|
||||
static inline uint32_t lean_int32_complement(uint32_t a) {
|
||||
int32_t arg = (int32_t)a;
|
||||
|
||||
return (uint32_t)(~arg);
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int32_dec_eq(uint32_t a1, uint32_t a2) {
|
||||
int32_t lhs = (int32_t)a1;
|
||||
int32_t rhs = (int32_t)a2;
|
||||
|
||||
return lhs == rhs;
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int32_dec_lt(uint32_t a1, uint32_t a2) {
|
||||
int32_t lhs = (int32_t)a1;
|
||||
int32_t rhs = (int32_t)a2;
|
||||
|
||||
return lhs < rhs;
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int32_dec_le(uint32_t a1, uint32_t a2) {
|
||||
int32_t lhs = (int32_t)a1;
|
||||
int32_t rhs = (int32_t)a2;
|
||||
|
||||
return lhs <= rhs;
|
||||
}
|
||||
|
||||
/* Int32 -> other */
|
||||
static inline uint8_t lean_int32_to_int8(uint32_t a) { return (uint8_t)(int8_t)(int32_t)a; }
|
||||
static inline uint16_t lean_int32_to_int16(uint32_t a) { return (uint16_t)(int16_t)(int32_t)a; }
|
||||
static inline uint64_t lean_int32_to_int64(uint32_t a) { return (uint64_t)(int64_t)(int32_t)a; }
|
||||
|
||||
/* Int64 */
|
||||
LEAN_EXPORT int64_t lean_int64_of_big_int(b_lean_obj_arg a);
|
||||
static inline uint64_t lean_int64_of_int(b_lean_obj_arg a) {
|
||||
int64_t res;
|
||||
|
||||
if (lean_is_scalar(a)) {
|
||||
res = lean_scalar_to_int64(a);
|
||||
} else {
|
||||
res = lean_int64_of_big_int(a);
|
||||
}
|
||||
|
||||
return (uint64_t)res;
|
||||
}
|
||||
|
||||
static inline uint64_t lean_int64_of_nat(b_lean_obj_arg a) {
|
||||
int64_t res;
|
||||
|
||||
if (lean_is_scalar(a)) {
|
||||
res = (int64_t)lean_unbox(a);
|
||||
} else {
|
||||
res = lean_int64_of_big_int(a);
|
||||
}
|
||||
|
||||
return (uint64_t)res;
|
||||
}
|
||||
|
||||
static inline lean_obj_res lean_int64_to_int_sint(uint64_t a) {
|
||||
int64_t arg = (int64_t)a;
|
||||
return lean_int64_to_int(arg);
|
||||
}
|
||||
|
||||
static inline uint64_t lean_int64_neg(uint64_t a) {
|
||||
int64_t arg = (int64_t)a;
|
||||
|
||||
return (uint64_t)(-arg);
|
||||
}
|
||||
|
||||
static inline uint64_t lean_int64_add(uint64_t a1, uint64_t a2) {
|
||||
int64_t lhs = (int64_t)a1;
|
||||
int64_t rhs = (int64_t)a2;
|
||||
|
||||
return (uint64_t)(lhs + rhs);
|
||||
}
|
||||
|
||||
static inline uint64_t lean_int64_sub(uint64_t a1, uint64_t a2) {
|
||||
int64_t lhs = (int64_t)a1;
|
||||
int64_t rhs = (int64_t)a2;
|
||||
|
||||
return (uint64_t)(lhs - rhs);
|
||||
}
|
||||
|
||||
static inline uint64_t lean_int64_mul(uint64_t a1, uint64_t a2) {
|
||||
int64_t lhs = (int64_t)a1;
|
||||
int64_t rhs = (int64_t)a2;
|
||||
|
||||
return (uint64_t)(lhs * rhs);
|
||||
}
|
||||
|
||||
static inline uint64_t lean_int64_div(uint64_t a1, uint64_t a2) {
|
||||
int64_t lhs = (int64_t)a1;
|
||||
int64_t rhs = (int64_t)a2;
|
||||
|
||||
return (uint64_t)(rhs == 0 ? 0 : lhs / rhs);
|
||||
}
|
||||
|
||||
static inline uint64_t lean_int64_mod(uint64_t a1, uint64_t a2) {
|
||||
int64_t lhs = (int64_t)a1;
|
||||
int64_t rhs = (int64_t)a2;
|
||||
|
||||
return (uint64_t)(rhs == 0 ? lhs : lhs % rhs);
|
||||
}
|
||||
|
||||
static inline uint64_t lean_int64_land(uint64_t a1, uint64_t a2) {
|
||||
int64_t lhs = (int64_t)a1;
|
||||
int64_t rhs = (int64_t)a2;
|
||||
|
||||
return (uint64_t)(lhs & rhs);
|
||||
}
|
||||
|
||||
static inline uint64_t lean_int64_lor(uint64_t a1, uint64_t a2) {
|
||||
int64_t lhs = (int64_t)a1;
|
||||
int64_t rhs = (int64_t)a2;
|
||||
|
||||
return (uint64_t)(lhs | rhs);
|
||||
}
|
||||
|
||||
static inline uint64_t lean_int64_xor(uint64_t a1, uint64_t a2) {
|
||||
int64_t lhs = (int64_t)a1;
|
||||
int64_t rhs = (int64_t)a2;
|
||||
|
||||
return (uint64_t)(lhs ^ rhs);
|
||||
}
|
||||
|
||||
static inline uint64_t lean_int64_shift_right(uint64_t a1, uint64_t a2) {
|
||||
int64_t lhs = (int64_t)a1;
|
||||
int64_t rhs = (((int64_t)a2 % 64) + 64) % 64; // this is smod 64
|
||||
|
||||
return (uint64_t)(lhs >> rhs);
|
||||
}
|
||||
|
||||
static inline uint64_t lean_int64_shift_left(uint64_t a1, uint64_t a2) {
|
||||
int64_t lhs = (int64_t)a1;
|
||||
int64_t rhs = (((int64_t)a2 % 64) + 64) % 64; // this is smod 64
|
||||
|
||||
return (uint64_t)(lhs << rhs);
|
||||
}
|
||||
|
||||
static inline uint64_t lean_int64_complement(uint64_t a) {
|
||||
int64_t arg = (int64_t)a;
|
||||
|
||||
return (uint64_t)(~arg);
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int64_dec_eq(uint64_t a1, uint64_t a2) {
|
||||
int64_t lhs = (int64_t)a1;
|
||||
int64_t rhs = (int64_t)a2;
|
||||
|
||||
return lhs == rhs;
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int64_dec_lt(uint64_t a1, uint64_t a2) {
|
||||
int64_t lhs = (int64_t)a1;
|
||||
int64_t rhs = (int64_t)a2;
|
||||
|
||||
return lhs < rhs;
|
||||
}
|
||||
|
||||
static inline uint8_t lean_int64_dec_le(uint64_t a1, uint64_t a2) {
|
||||
int64_t lhs = (int64_t)a1;
|
||||
int64_t rhs = (int64_t)a2;
|
||||
|
||||
return lhs <= rhs;
|
||||
}
|
||||
|
||||
/* Int64 -> other */
|
||||
static inline uint8_t lean_int64_to_int8(uint64_t a) { return (uint8_t)(int8_t)(int64_t)a; }
|
||||
static inline uint16_t lean_int64_to_int16(uint64_t a) { return (uint16_t)(int16_t)(int64_t)a; }
|
||||
static inline uint32_t lean_int64_to_int32(uint64_t a) { return (uint32_t)(int32_t)(int64_t)a; }
|
||||
|
||||
/* Float */
|
||||
|
||||
LEAN_EXPORT lean_obj_res lean_float_to_string(double a);
|
||||
|
||||
@@ -19,7 +19,10 @@ open Lean (Name)
|
||||
|
||||
/-- Compute a topological ordering of the package's transitive dependencies. -/
|
||||
def Package.recComputeDeps (self : Package) : FetchM (Array Package) := do
|
||||
(·.toArray) <$> self.deps.foldlM (init := OrdPackageSet.empty) fun deps dep => do
|
||||
(·.toArray) <$> self.depConfigs.foldlM (init := OrdPackageSet.empty) fun deps cfg => do
|
||||
let some dep ← findPackage? cfg.name
|
||||
| error s!"{self.name}: package not found for dependency '{cfg.name}' \
|
||||
(this is likely a bug in Lake)"
|
||||
return (← fetch <| dep.facet `deps).foldl (·.insert ·) deps |>.insert dep
|
||||
|
||||
/-- The `PackageFacetConfig` for the builtin `depsFacet`. -/
|
||||
|
||||
@@ -36,6 +36,10 @@ fetch functions, but not all fetch functions need build something.
|
||||
abbrev DFetchFn (α : Type u) (β : α → Type v) (m : Type v → Type w) :=
|
||||
(a : α) → m (β a)
|
||||
|
||||
/-- A `DFetchFn` that is not dependently typed. -/
|
||||
abbrev FetchFn (α : Type u) (β : Type v) (m : Type v → Type w) :=
|
||||
α → m β
|
||||
|
||||
/-!
|
||||
In order to nest builds / fetches within one another,
|
||||
we equip the monad `m` with a fetch function of its own.
|
||||
|
||||
@@ -41,12 +41,12 @@ BASIC OPTIONS:
|
||||
--help, -h print help of the program or a command and exit
|
||||
--dir, -d=file use the package configuration in a specific directory
|
||||
--file, -f=file use a specific file for the package configuration
|
||||
--lean=cmd specify the `lean` command used by Lake
|
||||
-K key[=value] set the configuration file option named key
|
||||
--old only rebuild modified modules (ignore transitive deps)
|
||||
--rehash, -H hash all files for traces (do not trust `.hash` files)
|
||||
--update, -U update manifest before building
|
||||
--update, -U update dependencies on load (e.g., before a build)
|
||||
--reconfigure, -R elaborate configuration files instead of using OLeans
|
||||
--keep-toolchain do not update toolchain on workspace update
|
||||
--no-build exit immediately if a build target is not up-to-date
|
||||
--no-cache build packages locally; do not download build caches
|
||||
--try-cache attempt to download build caches for supported packages
|
||||
|
||||
@@ -5,6 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
|
||||
-/
|
||||
import Lake.Util.Git
|
||||
import Lake.Util.Sugar
|
||||
import Lake.Util.Version
|
||||
import Lake.Config.Lang
|
||||
import Lake.Config.Package
|
||||
import Lake.Config.Workspace
|
||||
@@ -18,9 +19,6 @@ open Lean (Name)
|
||||
/-- The default module of an executable in `std` package. -/
|
||||
def defaultExeRoot : Name := `Main
|
||||
|
||||
/-- `elan` toolchain file name -/
|
||||
def toolchainFileName : FilePath := "lean-toolchain"
|
||||
|
||||
def gitignoreContents :=
|
||||
s!"/{defaultLakeDir}
|
||||
"
|
||||
|
||||
@@ -26,6 +26,7 @@ namespace Lake
|
||||
/-! ## General options for top-level `lake` -/
|
||||
|
||||
structure LakeOptions where
|
||||
args : List String := []
|
||||
rootDir : FilePath := "."
|
||||
configFile : FilePath := defaultConfigFile
|
||||
elanInstall? : Option ElanInstall := none
|
||||
@@ -36,6 +37,7 @@ structure LakeOptions where
|
||||
wantsHelp : Bool := false
|
||||
verbosity : Verbosity := .normal
|
||||
updateDeps : Bool := false
|
||||
updateToolchain : Bool := true
|
||||
reconfigure : Bool := false
|
||||
oldMode : Bool := false
|
||||
trustHash : Bool := true
|
||||
@@ -72,12 +74,15 @@ def LakeOptions.computeEnv (opts : LakeOptions) : EIO CliError Lake.Env := do
|
||||
/-- Make a `LoadConfig` from a `LakeOptions`. -/
|
||||
def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=
|
||||
return {
|
||||
lakeArgs? := opts.args.toArray
|
||||
lakeEnv := ← opts.computeEnv
|
||||
wsDir := opts.rootDir
|
||||
relConfigFile := opts.configFile
|
||||
lakeOpts := opts.configOpts
|
||||
leanOpts := Lean.Options.empty
|
||||
reconfigure := opts.reconfigure
|
||||
updateDeps := opts.updateDeps
|
||||
updateToolchain := opts.updateToolchain
|
||||
}
|
||||
|
||||
/-- Make a `BuildConfig` from a `LakeOptions`. -/
|
||||
@@ -101,7 +106,7 @@ abbrev CliM := ArgsT CliStateM
|
||||
|
||||
def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do
|
||||
let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
|
||||
let main := self.run' args |>.run' {elanInstall?, leanInstall?, lakeInstall?}
|
||||
let main := self.run' args |>.run' {args, elanInstall?, leanInstall?, lakeInstall?}
|
||||
let main := main.run >>= fun | .ok a => pure a | .error e => error e.toString
|
||||
main.run
|
||||
|
||||
@@ -111,6 +116,12 @@ def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do
|
||||
|
||||
instance (priority := low) : MonadLift LogIO CliStateM := ⟨CliStateM.runLogIO⟩
|
||||
|
||||
@[inline] def CliStateM.runLoggerIO (x : LoggerIO α) : CliStateM α := do
|
||||
let opts ← get
|
||||
MainM.runLoggerIO x opts.outLv opts.ansiMode
|
||||
|
||||
instance (priority := low) : MonadLift LoggerIO CliStateM := ⟨CliStateM.runLoggerIO⟩
|
||||
|
||||
/-! ## Argument Parsing -/
|
||||
|
||||
def takeArg (arg : String) : CliM String := do
|
||||
@@ -141,10 +152,6 @@ def noArgsRem (act : CliStateM α) : CliM α := do
|
||||
def getWantsHelp : CliStateM Bool :=
|
||||
(·.wantsHelp) <$> get
|
||||
|
||||
def setLean (lean : String) : CliStateM PUnit := do
|
||||
let leanInstall? ← findLeanCmdInstall? lean
|
||||
modify ({· with leanInstall?})
|
||||
|
||||
def setConfigOpt (kvPair : String) : CliM PUnit :=
|
||||
let pos := kvPair.posOf '='
|
||||
let (key, val) :=
|
||||
@@ -171,6 +178,7 @@ def lakeLongOption : (opt : String) → CliM PUnit
|
||||
| "--quiet" => modifyThe LakeOptions ({· with verbosity := .quiet})
|
||||
| "--verbose" => modifyThe LakeOptions ({· with verbosity := .verbose})
|
||||
| "--update" => modifyThe LakeOptions ({· with updateDeps := true})
|
||||
| "--keep-toolchain" => modifyThe LakeOptions ({· with updateToolchain := false})
|
||||
| "--reconfigure" => modifyThe LakeOptions ({· with reconfigure := true})
|
||||
| "--old" => modifyThe LakeOptions ({· with oldMode := true})
|
||||
| "--no-build" => modifyThe LakeOptions ({· with noBuild := true})
|
||||
@@ -193,7 +201,6 @@ def lakeLongOption : (opt : String) → CliM PUnit
|
||||
| "--file" => do
|
||||
let configFile ← takeOptArg "--file" "path"
|
||||
modifyThe LakeOptions ({· with configFile})
|
||||
| "--lean" => do setLean <| ← takeOptArg "--lean" "path or command"
|
||||
| "--help" => modifyThe LakeOptions ({· with wantsHelp := true})
|
||||
| "--" => do
|
||||
let subArgs ← takeArgs
|
||||
@@ -331,7 +338,7 @@ protected def build : CliM PUnit := do
|
||||
processOptions lakeOption
|
||||
let opts ← getThe LakeOptions
|
||||
let config ← mkLoadConfig opts
|
||||
let ws ← loadWorkspace config opts.updateDeps
|
||||
let ws ← loadWorkspace config
|
||||
let targetSpecs ← takeArgs
|
||||
let specs ← parseTargetSpecs ws targetSpecs
|
||||
let buildConfig := mkBuildConfig opts (out := .stdout)
|
||||
@@ -350,7 +357,7 @@ protected def resolveDeps : CliM PUnit := do
|
||||
let opts ← getThe LakeOptions
|
||||
let config ← mkLoadConfig opts
|
||||
noArgsRem do
|
||||
discard <| loadWorkspace config opts.updateDeps
|
||||
discard <| loadWorkspace config
|
||||
|
||||
protected def update : CliM PUnit := do
|
||||
processOptions lakeOption
|
||||
|
||||
@@ -38,7 +38,7 @@ def setupFile
|
||||
IO.eprintln s!"Invalid Lake configuration. Please restart the server after fixing the Lake configuration file."
|
||||
exit 1
|
||||
let outLv := buildConfig.verbosity.minLogLv
|
||||
let ws ← MainM.runLogIO (minLv := outLv) (ansiMode := .noAnsi) do
|
||||
let ws ← MainM.runLoggerIO (minLv := outLv) (ansiMode := .noAnsi) do
|
||||
loadWorkspace loadConfig
|
||||
let imports := imports.foldl (init := #[]) fun imps imp =>
|
||||
if let some mod := ws.findModule? imp.toName then imps.push mod else imps
|
||||
@@ -71,7 +71,7 @@ with the given additional `args`.
|
||||
-/
|
||||
def serve (config : LoadConfig) (args : Array String) : IO UInt32 := do
|
||||
let (extraEnv, moreServerArgs) ← do
|
||||
let (ws?, log) ← (loadWorkspace config).run?
|
||||
let (ws?, log) ← (loadWorkspace config).captureLog
|
||||
log.replay (logger := MonadLog.stderr)
|
||||
if let some ws := ws? then
|
||||
let ctx := mkLakeContext ws
|
||||
|
||||
@@ -63,7 +63,7 @@ def compute
|
||||
lake, lean, elan?,
|
||||
pkgUrlMap := ← computePkgUrlMap
|
||||
reservoirApiUrl := ← getUrlD "RESERVOIR_API_URL" s!"{reservoirBaseUrl}/v1"
|
||||
noCache := (noCache <|> (← IO.getEnv "LAKE_NO_CACHE").bind toBool?).getD false
|
||||
noCache := (noCache <|> (← IO.getEnv "LAKE_NO_CACHE").bind envToBool?).getD false
|
||||
githashOverride := (← IO.getEnv "LEAN_GITHASH").getD ""
|
||||
initToolchain := (← IO.getEnv "ELAN_TOOLCHAIN").getD ""
|
||||
initLeanPath := ← getSearchPath "LEAN_PATH",
|
||||
@@ -72,10 +72,6 @@ def compute
|
||||
initPath := ← getSearchPath "PATH"
|
||||
}
|
||||
where
|
||||
toBool? (o : String) : Option Bool :=
|
||||
if ["y", "yes", "t", "true", "on", "1"].contains o.toLower then true
|
||||
else if ["n", "no", "f", "false", "off", "0"].contains o.toLower then false
|
||||
else none
|
||||
computePkgUrlMap := do
|
||||
let some urlMapStr ← IO.getEnv "LAKE_PKG_URL_MAP" | return {}
|
||||
match Json.parse urlMapStr |>.bind fromJson? with
|
||||
@@ -144,14 +140,29 @@ Combines the initial path of the environment with that of the Lean installation.
|
||||
def sharedLibPath (env : Env) : SearchPath :=
|
||||
env.lean.sharedLibPath ++ env.initSharedLibPath
|
||||
|
||||
/-- Unset toolchain-specific environment variables. -/
|
||||
def noToolchainVars : Array (String × Option String) :=
|
||||
#[
|
||||
("ELAN_TOOLCHAIN", none),
|
||||
("LAKE", none),
|
||||
("LAKE_OVERRIDE_LEAN", none),
|
||||
("LAKE_HOME", none),
|
||||
("LEAN", none),
|
||||
("LEAN_GITHASH", none),
|
||||
("LEAN_SYSROOT", none),
|
||||
("LEAN_AR", none)
|
||||
]
|
||||
|
||||
/-- Environment variable settings that are not augmented by a Lake workspace. -/
|
||||
def baseVars (env : Env) : Array (String × Option String) :=
|
||||
#[
|
||||
("ELAN", env.elan?.map (·.elan.toString)),
|
||||
("ELAN_HOME", env.elan?.map (·.home.toString)),
|
||||
("ELAN_TOOLCHAIN", if env.toolchain.isEmpty then none else env.toolchain),
|
||||
("LAKE", env.lake.lake.toString),
|
||||
("LAKE_HOME", env.lake.home.toString),
|
||||
("LAKE_PKG_URL_MAP", toJson env.pkgUrlMap |>.compress),
|
||||
("LEAN", env.lean.lean.toString),
|
||||
("LEAN_GITHASH", env.leanGithash),
|
||||
("LEAN_SYSROOT", env.lean.sysroot.toString),
|
||||
("LEAN_AR", env.lean.ar.toString),
|
||||
|
||||
@@ -9,16 +9,18 @@ import Lake.Config.Defaults
|
||||
open System
|
||||
namespace Lake
|
||||
|
||||
/-! ## Data Structures -/
|
||||
/-- Convert the string value of an environment variable to a boolean. -/
|
||||
def envToBool? (o : String) : Option Bool :=
|
||||
if ["y", "yes", "t", "true", "on", "1"].contains o.toLower then true
|
||||
else if ["n", "no", "f", "false", "off", "0"].contains o.toLower then false
|
||||
else none
|
||||
|
||||
/-- Standard path of `elan` in a Elan installation. -/
|
||||
def elanExe (home : FilePath) :=
|
||||
home / "bin" / "elan" |>.addExtension FilePath.exeExtension
|
||||
/-! ## Data Structures -/
|
||||
|
||||
/-- Information about the local Elan setup. -/
|
||||
structure ElanInstall where
|
||||
home : FilePath
|
||||
elan := elanExe home
|
||||
elan : FilePath
|
||||
binDir := home / "bin"
|
||||
toolchainsDir := home / "toolchains"
|
||||
deriving Inhabited, Repr
|
||||
@@ -57,7 +59,7 @@ def initSharedLib : FilePath :=
|
||||
/-- Path information about the local Lean installation. -/
|
||||
structure LeanInstall where
|
||||
sysroot : FilePath
|
||||
githash : String
|
||||
githash : String := ""
|
||||
srcDir := sysroot / "src" / "lean"
|
||||
leanLibDir := sysroot / "lib" / "lean"
|
||||
includeDir := sysroot / "include"
|
||||
@@ -67,9 +69,9 @@ structure LeanInstall where
|
||||
leanc := leancExe sysroot
|
||||
sharedLib := leanSharedLibDir sysroot / leanSharedLib
|
||||
initSharedLib := leanSharedLibDir sysroot / initSharedLib
|
||||
ar : FilePath
|
||||
cc : FilePath
|
||||
customCc : Bool
|
||||
ar : FilePath := "ar"
|
||||
cc : FilePath := "cc"
|
||||
customCc : Bool := false
|
||||
deriving Inhabited, Repr
|
||||
|
||||
/--
|
||||
@@ -110,12 +112,16 @@ def LakeInstall.ofLean (lean : LeanInstall) : LakeInstall where
|
||||
/-! ## Detection Functions -/
|
||||
|
||||
/--
|
||||
Attempt to detect a Elan installation by checking the `ELAN_HOME`
|
||||
environment variable for a installation location.
|
||||
Attempt to detect an Elan installation by checking the `ELAN` and `ELAN_HOME`
|
||||
environment variables. If `ELAN` is set but empty, Elan is considered disabled.
|
||||
-/
|
||||
def findElanInstall? : BaseIO (Option ElanInstall) := do
|
||||
if let some home ← IO.getEnv "ELAN_HOME" then
|
||||
return some {home}
|
||||
let elan := (← IO.getEnv "ELAN").getD "elan"
|
||||
if elan.trim.isEmpty then
|
||||
return none
|
||||
else
|
||||
return some {elan, home}
|
||||
return none
|
||||
|
||||
/--
|
||||
@@ -149,9 +155,9 @@ set to the empty string.
|
||||
|
||||
For (2), if `LEAN_AR` or `LEAN_CC` are defined, it uses those paths.
|
||||
Otherwise, if Lean is packaged with an `llvm-ar` and/or `clang`, use them.
|
||||
If not, use the `ar` and/or `cc` in the system's `PATH`. This last step is
|
||||
needed because internal builds of Lean do not bundle these tools
|
||||
(unlike user-facing releases).
|
||||
If not, use the `ar` and/or `cc` from the `AR` / `CC` environment variables
|
||||
or the system's `PATH`. This last step is needed because internal builds of
|
||||
Lean do not bundle these tools (unlike user-facing releases).
|
||||
|
||||
We also track whether `LEAN_CC` was set to determine whether it should
|
||||
be set in the future for `lake env`. This is because if `LEAN_CC` was not set,
|
||||
@@ -187,18 +193,29 @@ where
|
||||
return FilePath.mk ar
|
||||
else
|
||||
let ar := leanArExe sysroot
|
||||
if (← ar.pathExists) then pure ar else pure "ar"
|
||||
if (← ar.pathExists) then
|
||||
return ar
|
||||
else if let some ar ← IO.getEnv "AR" then
|
||||
return ar
|
||||
else
|
||||
return "ar"
|
||||
findCc := do
|
||||
if let some cc ← IO.getEnv "LEAN_CC" then
|
||||
return (FilePath.mk cc, true)
|
||||
else
|
||||
let cc := leanCcExe sysroot
|
||||
let cc := if (← cc.pathExists) then cc else "cc"
|
||||
let cc ←
|
||||
if (← cc.pathExists) then
|
||||
pure cc
|
||||
else if let some cc ← IO.getEnv "CC" then
|
||||
pure cc
|
||||
else
|
||||
pure "cc"
|
||||
return (cc, false)
|
||||
|
||||
/--
|
||||
Attempt to detect the installation of the given `lean` command
|
||||
by calling `findLeanCmdHome?`. See `LeanInstall.get` for how it assumes the
|
||||
by calling `findLeanSysroot?`. See `LeanInstall.get` for how it assumes the
|
||||
Lean install is organized.
|
||||
-/
|
||||
def findLeanCmdInstall? (lean := "lean") : BaseIO (Option LeanInstall) :=
|
||||
@@ -235,14 +252,28 @@ def getLakeInstall? (lake : FilePath) : BaseIO (Option LakeInstall) := do
|
||||
return none
|
||||
|
||||
/--
|
||||
Attempt to detect Lean's installation by first checking the
|
||||
`LEAN_SYSROOT` environment variable and then by trying `findLeanCmdHome?`.
|
||||
Attempt to detect Lean's installation by using the `LEAN` and `LEAN_SYSROOT`
|
||||
environment variables.
|
||||
|
||||
If `LEAN_SYSROOT` is set, use it. Otherwise, check `LEAN` for the `lean`
|
||||
executable. If `LEAN` is set but empty, Lean will be considered disabled.
|
||||
Otherwise, Lean's location will be determined by trying `findLeanSysroot?`
|
||||
using value of `LEAN` or, if unset, the `lean` in `PATH`.
|
||||
|
||||
See `LeanInstall.get` for how it assumes the Lean install is organized.
|
||||
-/
|
||||
def findLeanInstall? : BaseIO (Option LeanInstall) := do
|
||||
if let some sysroot ← IO.getEnv "LEAN_SYSROOT" then
|
||||
return some <| ← LeanInstall.get sysroot
|
||||
if let some sysroot ← findLeanSysroot? then
|
||||
let lean ← do
|
||||
if let some lean ← IO.getEnv "LEAN" then
|
||||
if lean.trim.isEmpty then
|
||||
return none
|
||||
else
|
||||
pure lean
|
||||
else
|
||||
pure "lean"
|
||||
if let some sysroot ← findLeanSysroot? lean then
|
||||
return some <| ← LeanInstall.get sysroot
|
||||
return none
|
||||
|
||||
@@ -271,7 +302,8 @@ Then it attempts to detect if Lake and Lean are part of a single installation
|
||||
where the `lake` executable is co-located with the `lean` executable (i.e., they
|
||||
are in the same directory). If Lean and Lake are not co-located, Lake will
|
||||
attempt to find the their installations separately by calling
|
||||
`findLeanInstall?` and `findLakeInstall?`.
|
||||
`findLeanInstall?` and `findLakeInstall?`. Setting `LAKE_OVERRIDE_LEAN` to true
|
||||
will force Lake to use `findLeanInstall?` even if co-located.
|
||||
|
||||
When co-located, Lake will assume that Lean and Lake's binaries are located in
|
||||
`<sysroot>/bin`, their Lean libraries in `<sysroot>/lib/lean`, Lean's source files
|
||||
@@ -280,9 +312,13 @@ following the pattern of a regular Lean toolchain.
|
||||
-/
|
||||
def findInstall? : BaseIO (Option ElanInstall × Option LeanInstall × Option LakeInstall) := do
|
||||
let elan? ← findElanInstall?
|
||||
if let some home ← findLakeLeanJointHome? then
|
||||
let lean ← LeanInstall.get home (collocated := true)
|
||||
let lake := LakeInstall.ofLean lean
|
||||
return (elan?, lean, lake)
|
||||
if let some sysroot ← findLakeLeanJointHome? then
|
||||
if (← IO.getEnv "LAKE_OVERRIDE_LEAN").bind envToBool? |>.getD false then
|
||||
let lake := LakeInstall.ofLean {sysroot}
|
||||
return (elan?, ← findLeanInstall?, lake)
|
||||
else
|
||||
let lean ← LeanInstall.get sysroot (collocated := true)
|
||||
let lake := LakeInstall.ofLean lean
|
||||
return (elan?, lean, lake)
|
||||
else
|
||||
return (elan?, ← findLeanInstall?, ← findLakeInstall?)
|
||||
|
||||
@@ -45,6 +45,10 @@ abbrev MonadLake (m : Type → Type u) :=
|
||||
@[inline] def mkLakeContext (ws : Workspace) : Lake.Context where
|
||||
opaqueWs := ws
|
||||
|
||||
/-- Run a `LakeT` monad in the context of this workspace. -/
|
||||
@[inline] def Workspace.runLakeT (ws : Workspace) (x : LakeT m α) : m α :=
|
||||
x.run (mkLakeContext ws)
|
||||
|
||||
instance [MonadWorkspace m] [Functor m] : MonadLake m where
|
||||
read := (mkLakeContext ·) <$> getWorkspace
|
||||
|
||||
|
||||
@@ -8,9 +8,6 @@ import Lake.Util.Opaque
|
||||
|
||||
namespace Lake
|
||||
|
||||
/-- Opaque reference to a `Package` used for forward declaration. -/
|
||||
declare_opaque_type OpaquePackage
|
||||
|
||||
/-- Opaque reference to a `Workspace` used for forward declaration. -/
|
||||
declare_opaque_type OpaqueWorkspace
|
||||
|
||||
|
||||
@@ -380,11 +380,9 @@ structure Package where
|
||||
/-- The path to the package's JSON manifest of remote dependencies (relative to `dir`). -/
|
||||
relManifestFile : FilePath := config.manifestFile.getD defaultManifestFile
|
||||
/-- The package's scope (e.g., in Reservoir). -/
|
||||
scope : String := ""
|
||||
scope : String
|
||||
/-- The URL to this package's Git remote. -/
|
||||
remoteUrl : String := ""
|
||||
/-- (Opaque references to) the package's direct dependencies. -/
|
||||
opaqueDeps : Array OpaquePackage := #[]
|
||||
remoteUrl : String
|
||||
/-- Dependency configurations for the package. -/
|
||||
depConfigs : Array Dependency := #[]
|
||||
/-- Lean library configurations for the package. -/
|
||||
@@ -419,8 +417,6 @@ instance : Nonempty Package :=
|
||||
have : Inhabited Environment := Classical.inhabited_of_nonempty inferInstance
|
||||
⟨by constructor <;> exact default⟩
|
||||
|
||||
hydrate_opaque_type OpaquePackage Package
|
||||
|
||||
instance : Hashable Package where hash pkg := hash pkg.config.name
|
||||
instance : BEq Package where beq p1 p2 := p1.config.name == p2.config.name
|
||||
|
||||
@@ -508,10 +504,6 @@ namespace Package
|
||||
@[inline] def readmeFile (self : Package) : FilePath :=
|
||||
self.dir / self.config.readmeFile
|
||||
|
||||
/-- The package's direct dependencies. -/
|
||||
@[inline] def deps (self : Package) : Array Package :=
|
||||
self.opaqueDeps.map (·.get)
|
||||
|
||||
/-- The path to the package's Lake directory relative to `dir` (e.g., `.lake`). -/
|
||||
@[inline] def relLakeDir (_ : Package) : FilePath :=
|
||||
defaultLakeDir
|
||||
|
||||
@@ -18,8 +18,14 @@ open Lean (Name)
|
||||
structure Workspace : Type where
|
||||
/-- The root package of the workspace. -/
|
||||
root : Package
|
||||
/-- The detect `Lake.Env` of the workspace. -/
|
||||
/-- The detected `Lake.Env` of the workspace. -/
|
||||
lakeEnv : Lake.Env
|
||||
/--
|
||||
The CLI arguments Lake was run with.
|
||||
Used by `lake update` to perform a restart of Lake on a toolchain update.
|
||||
A value of `none` means that Lake is not restartable via the CLI.
|
||||
-/
|
||||
lakeArgs? : Option (Array String) := none
|
||||
/-- The packages within the workspace (in `require` declaration order). -/
|
||||
packages : Array Package := {}
|
||||
/-- Name-package map of packages within the workspace. -/
|
||||
@@ -77,7 +83,7 @@ def addPackage (pkg : Package) (self : Workspace) : Workspace :=
|
||||
|
||||
/-- Try to find a script in the workspace with the given name. -/
|
||||
protected def findScript? (script : Name) (self : Workspace) : Option Script :=
|
||||
self.packages.findSomeRev? (·.scripts.find? script)
|
||||
self.packages.findSome? (·.scripts.find? script)
|
||||
|
||||
/-- Check if the module is local to any package in the workspace. -/
|
||||
def isLocalModule (mod : Name) (self : Workspace) : Bool :=
|
||||
@@ -89,27 +95,27 @@ def isBuildableModule (mod : Name) (self : Workspace) : Bool :=
|
||||
|
||||
/-- Locate the named, buildable, importable, local module in the workspace. -/
|
||||
protected def findModule? (mod : Name) (self : Workspace) : Option Module :=
|
||||
self.packages.findSomeRev? (·.findModule? mod)
|
||||
self.packages.findSome? (·.findModule? mod)
|
||||
|
||||
/-- Locate the named, buildable, but not necessarily importable, module in the workspace. -/
|
||||
def findTargetModule? (mod : Name) (self : Workspace) : Option Module :=
|
||||
self.packages.findSomeRev? (·.findTargetModule? mod)
|
||||
self.packages.findSome? (·.findTargetModule? mod)
|
||||
|
||||
/-- Try to find a Lean library in the workspace with the given name. -/
|
||||
protected def findLeanLib? (name : Name) (self : Workspace) : Option LeanLib :=
|
||||
self.packages.findSomeRev? fun pkg => pkg.findLeanLib? name
|
||||
self.packages.findSome? fun pkg => pkg.findLeanLib? name
|
||||
|
||||
/-- Try to find a Lean executable in the workspace with the given name. -/
|
||||
protected def findLeanExe? (name : Name) (self : Workspace) : Option LeanExe :=
|
||||
self.packages.findSomeRev? fun pkg => pkg.findLeanExe? name
|
||||
self.packages.findSome? fun pkg => pkg.findLeanExe? name
|
||||
|
||||
/-- Try to find an external library in the workspace with the given name. -/
|
||||
protected def findExternLib? (name : Name) (self : Workspace) : Option ExternLib :=
|
||||
self.packages.findSomeRev? fun pkg => pkg.findExternLib? name
|
||||
self.packages.findSome? fun pkg => pkg.findExternLib? name
|
||||
|
||||
/-- Try to find a target configuration in the workspace with the given name. -/
|
||||
def findTargetConfig? (name : Name) (self : Workspace) : Option ((pkg : Package) × TargetConfig pkg.name name) :=
|
||||
self.packages.findSomeRev? fun pkg => pkg.findTargetConfig? name <&> (⟨pkg, ·⟩)
|
||||
self.packages.findSome? fun pkg => pkg.findTargetConfig? name <&> (⟨pkg, ·⟩)
|
||||
|
||||
/-- Add a module facet to the workspace. -/
|
||||
def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace :=
|
||||
@@ -137,15 +143,15 @@ def findLibraryFacetConfig? (name : Name) (self : Workspace) : Option (LibraryFa
|
||||
|
||||
/-- The workspace's binary directories (which are added to `Path`). -/
|
||||
def binPath (self : Workspace) : SearchPath :=
|
||||
self.packages.foldr (fun pkg dirs => pkg.binDir :: dirs) []
|
||||
self.packages.foldl (fun dirs pkg => pkg.binDir :: dirs) []
|
||||
|
||||
/-- The workspace's Lean library directories (which are added to `LEAN_PATH`). -/
|
||||
def leanPath (self : Workspace) : SearchPath :=
|
||||
self.packages.foldr (fun pkg dirs => pkg.leanLibDir :: dirs) []
|
||||
self.packages.foldl (fun dirs pkg => pkg.leanLibDir :: dirs) []
|
||||
|
||||
/-- The workspace's source directories (which are added to `LEAN_SRC_PATH`). -/
|
||||
def leanSrcPath (self : Workspace) : SearchPath :=
|
||||
self.packages.foldr (init := {}) fun pkg dirs =>
|
||||
self.packages.foldl (init := {}) fun dirs pkg =>
|
||||
pkg.leanLibConfigs.foldr (init := dirs) fun cfg dirs =>
|
||||
pkg.srcDir / cfg.srcDir :: dirs
|
||||
|
||||
|
||||
@@ -8,6 +8,7 @@ import Lean.Data.Options
|
||||
import Lake.Config.Defaults
|
||||
import Lake.Config.Env
|
||||
import Lake.Util.Log
|
||||
import Lake.Util.Version
|
||||
|
||||
namespace Lake
|
||||
open System Lean
|
||||
@@ -16,6 +17,12 @@ open System Lean
|
||||
structure LoadConfig where
|
||||
/-- The Lake environment of the load process. -/
|
||||
lakeEnv : Lake.Env
|
||||
/--
|
||||
The CLI arguments Lake was run with.
|
||||
Used to perform a restart of Lake on a toolchain update.
|
||||
A value of `none` means that Lake is not restartable via the CLI.
|
||||
-/
|
||||
lakeArgs? : Option (Array String) := none
|
||||
/-- The root directory of the Lake workspace. -/
|
||||
wsDir : FilePath
|
||||
/-- The directory of the loaded package (relative to the root). -/
|
||||
@@ -26,8 +33,15 @@ structure LoadConfig where
|
||||
lakeOpts : NameMap String := {}
|
||||
/-- The Lean options with which to elaborate the configuration file. -/
|
||||
leanOpts : Options := {}
|
||||
/-- If `true`, Lake will elaborate configuration files instead of using OLeans. -/
|
||||
/-- Whether Lake should re-elaborate configuration files instead of using cached OLeans. -/
|
||||
reconfigure : Bool := false
|
||||
/-- Whether to update dependencies when loading the workspace. -/
|
||||
updateDeps : Bool := false
|
||||
/--
|
||||
Whether to update the workspace's `lean-toolchain` when dependencies are updated.
|
||||
If `true` and a toolchain update occurs, Lake will need to be restarted.
|
||||
-/
|
||||
updateToolchain : Bool := true
|
||||
/-- The package's scope (e.g., in Reservoir). -/
|
||||
scope : String := ""
|
||||
/-- The URL to this package's Git remote (if any). -/
|
||||
|
||||
@@ -20,31 +20,36 @@ or resolve a local path dependency.
|
||||
namespace Lake
|
||||
|
||||
/-- Update the Git package in `repo` to `rev` if not already at it. -/
|
||||
def updateGitPkg (name : String) (repo : GitRepo) (rev? : Option String) : LogIO PUnit := do
|
||||
def updateGitPkg
|
||||
(name : String) (repo : GitRepo) (rev? : Option String)
|
||||
: LogIO PUnit := do
|
||||
let rev ← repo.findRemoteRevision rev?
|
||||
if (← repo.getHeadRevision) = rev then
|
||||
if (← repo.hasDiff) then
|
||||
logWarning s!"{name}: repository '{repo.dir}' has local changes"
|
||||
else
|
||||
logInfo s!"{name}: updating repository '{repo.dir}' to revision '{rev}'"
|
||||
logInfo s!"{name}: checking out revision '{rev}'"
|
||||
repo.checkoutDetach rev
|
||||
|
||||
/-- Clone the Git package as `repo`. -/
|
||||
def cloneGitPkg (name : String) (repo : GitRepo)
|
||||
(url : String) (rev? : Option String) : LogIO PUnit := do
|
||||
logInfo s!"{name}: cloning {url} to '{repo.dir}'"
|
||||
def cloneGitPkg
|
||||
(name : String) (repo : GitRepo) (url : String) (rev? : Option String)
|
||||
: LogIO PUnit := do
|
||||
logInfo s!"{name}: cloning {url}"
|
||||
repo.clone url
|
||||
if let some rev := rev? then
|
||||
let hash ← repo.resolveRemoteRevision rev
|
||||
repo.checkoutDetach hash
|
||||
let rev ← repo.resolveRemoteRevision rev
|
||||
logInfo s!"{name}: checking out revision '{rev}'"
|
||||
repo.checkoutDetach rev
|
||||
|
||||
/--
|
||||
Update the Git repository from `url` in `repo` to `rev?`.
|
||||
If `repo` is already from `url`, just checkout the new revision.
|
||||
Otherwise, delete the local repository and clone a fresh copy from `url`.
|
||||
-/
|
||||
def updateGitRepo (name : String) (repo : GitRepo)
|
||||
(url : String) (rev? : Option String) : LogIO Unit := do
|
||||
def updateGitRepo
|
||||
(name : String) (repo : GitRepo) (url : String) (rev? : Option String)
|
||||
: LogIO Unit := do
|
||||
let sameUrl ← EIO.catchExceptions (h := fun _ => pure false) <| show IO Bool from do
|
||||
let some remoteUrl ← repo.getRemoteUrl? | return false
|
||||
if remoteUrl = url then return true
|
||||
@@ -65,8 +70,9 @@ def updateGitRepo (name : String) (repo : GitRepo)
|
||||
Materialize the Git repository from `url` into `repo` at `rev?`.
|
||||
Clone it if no local copy exists, otherwise update it.
|
||||
-/
|
||||
def materializeGitRepo (name : String) (repo : GitRepo)
|
||||
(url : String) (rev? : Option String) : LogIO Unit := do
|
||||
def materializeGitRepo
|
||||
(name : String) (repo : GitRepo) (url : String) (rev? : Option String)
|
||||
: LogIO Unit := do
|
||||
if (← repo.dirExists) then
|
||||
updateGitRepo name repo url rev?
|
||||
else
|
||||
@@ -110,11 +116,7 @@ def Dependency.materialize
|
||||
match src with
|
||||
| .path dir =>
|
||||
let relPkgDir := relParentDir / dir
|
||||
return {
|
||||
relPkgDir
|
||||
remoteUrl := ""
|
||||
manifestEntry := mkEntry <| .path relPkgDir
|
||||
}
|
||||
return mkDep relPkgDir "" (.path relPkgDir)
|
||||
| .git url inputRev? subDir? => do
|
||||
let sname := dep.name.toString (escape := false)
|
||||
let repoUrl := Git.filterUrl? url |>.getD ""
|
||||
@@ -127,7 +129,7 @@ def Dependency.materialize
|
||||
if ver.startsWith "git#" then
|
||||
return ver.drop 4
|
||||
else
|
||||
error s!"{dep.name} unsupported dependency version format '{ver}' (should be \"git#>rev>\")"
|
||||
error s!"{dep.name}: unsupported dependency version format '{ver}' (should be \"git#>rev>\")"
|
||||
let depName := dep.name.toString (escape := false)
|
||||
let some pkg ← Reservoir.fetchPkg? lakeEnv dep.scope depName
|
||||
| error s!"{dep.scope}/{depName}: could not materialize package: \
|
||||
@@ -139,18 +141,17 @@ def Dependency.materialize
|
||||
(githubUrl?.getD "") (verRev? <|> defaultBranch?) subDir?
|
||||
| _ => error s!"{pkg.fullName}: Git source not found on Reservoir"
|
||||
where
|
||||
mkEntry src : PackageEntry :=
|
||||
{name := dep.name, scope := dep.scope, inherited, src}
|
||||
materializeGit name relPkgDir gitUrl remoteUrl inputRev? subDir? : LogIO MaterializedDep := do
|
||||
let repo := GitRepo.mk (wsDir / relPkgDir)
|
||||
let gitUrl := lakeEnv.pkgUrlMap.find? dep.name |>.getD gitUrl
|
||||
materializeGitRepo name repo gitUrl inputRev?
|
||||
let rev ← repo.getHeadRevision
|
||||
let relPkgDir := if let some subDir := subDir? then relPkgDir / subDir else relPkgDir
|
||||
return {
|
||||
relPkgDir, remoteUrl
|
||||
manifestEntry := mkEntry <| .git gitUrl rev inputRev? subDir?
|
||||
}
|
||||
return mkDep relPkgDir remoteUrl <| .git gitUrl rev inputRev? subDir?
|
||||
@[inline] mkDep relPkgDir remoteUrl src : MaterializedDep := {
|
||||
relPkgDir, remoteUrl,
|
||||
manifestEntry := {name := dep.name, scope := dep.scope, inherited, src}
|
||||
}
|
||||
|
||||
/--
|
||||
Materializes a manifest package entry, cloning and/or checking it out as necessary.
|
||||
@@ -161,11 +162,7 @@ def PackageEntry.materialize
|
||||
: LogIO MaterializedDep :=
|
||||
match manifestEntry.src with
|
||||
| .path (dir := relPkgDir) .. =>
|
||||
return {
|
||||
relPkgDir
|
||||
remoteUrl := ""
|
||||
manifestEntry
|
||||
}
|
||||
return mkDep relPkgDir ""
|
||||
| .git (url := url) (rev := rev) (subDir? := subDir?) .. => do
|
||||
let sname := manifestEntry.name.toString (escape := false)
|
||||
let relGitDir := relPkgsDir / sname
|
||||
@@ -188,8 +185,7 @@ def PackageEntry.materialize
|
||||
let url := lakeEnv.pkgUrlMap.find? manifestEntry.name |>.getD url
|
||||
cloneGitPkg sname repo url rev
|
||||
let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
|
||||
return {
|
||||
relPkgDir
|
||||
remoteUrl := Git.filterUrl? url |>.getD ""
|
||||
manifestEntry
|
||||
}
|
||||
return mkDep relPkgDir (Git.filterUrl? url |>.getD "")
|
||||
where
|
||||
@[inline] mkDep relPkgDir remoteUrl : MaterializedDep :=
|
||||
{relPkgDir, remoteUrl, manifestEntry}
|
||||
|
||||
@@ -18,6 +18,21 @@ This module contains definitions for resolving the dependencies of a package.
|
||||
|
||||
namespace Lake
|
||||
|
||||
def stdMismatchError (newName : String) (rev : String) :=
|
||||
s!"the 'std' package has been renamed to '{newName}' and moved to the
|
||||
'leanprover-community' organization; downstream packages which wish to
|
||||
update to the new std should replace
|
||||
|
||||
require std from
|
||||
git \"https://github.com/leanprover/std4\"{rev}
|
||||
|
||||
in their Lake configuration file with
|
||||
|
||||
require {newName} from
|
||||
git \"https://github.com/leanprover-community/{newName}\"{rev}
|
||||
|
||||
"
|
||||
|
||||
/--
|
||||
Loads the package configuration of a materialized dependency.
|
||||
Adds the facets defined in the package to the `Workspace`.
|
||||
@@ -43,100 +58,82 @@ def loadDepPackage
|
||||
else
|
||||
return (pkg, ws)
|
||||
|
||||
/-- The monad of the dependency resolver. -/
|
||||
abbrev ResolveT m := CallStackT Name <| StateT Workspace m
|
||||
/--
|
||||
The resolver's call stack of dependencies.
|
||||
That is, the dependency currently being resolved plus its parents.
|
||||
-/
|
||||
abbrev DepStack := CallStack Name
|
||||
|
||||
@[inline] nonrec def ResolveT.run (ws : Workspace) (x : ResolveT m α) (stack : CallStack Name := {}) : m (α × Workspace) :=
|
||||
x.run stack |>.run ws
|
||||
/--
|
||||
A monad transformer for recursive dependency resolution.
|
||||
It equips the monad with the stack of dependencies currently being resolved.
|
||||
-/
|
||||
abbrev DepStackT m := CallStackT Name m
|
||||
|
||||
@[inline] nonrec def DepStackT.run
|
||||
(x : DepStackT m α) (stack : DepStack := {})
|
||||
: m α :=
|
||||
x.run stack
|
||||
|
||||
/-- Log dependency cycle and error. -/
|
||||
@[specialize] def depCycleError [MonadError m] (cycle : Cycle Name) : m α :=
|
||||
error s!"dependency cycle detected:\n{"\n".intercalate <| cycle.map (s!" {·}")}"
|
||||
|
||||
instance [Monad m] [MonadError m] : MonadCycleOf Name (ResolveT m) where
|
||||
instance [Monad m] [MonadError m] : MonadCycleOf Name (DepStackT m) where
|
||||
throwCycle := depCycleError
|
||||
|
||||
/--
|
||||
Recursively visits the workspace dependency graph, starting from `root`.
|
||||
At each package, loops through each direct dependency performing just `breath`.
|
||||
Them, loops again through the results applying `depth`, recursing, and adding
|
||||
the package to workspace's package set. Errors if a cycle is encountered.
|
||||
/-- The monad of the dependency resolver. -/
|
||||
abbrev ResolveT m := DepStackT <| StateT Workspace m
|
||||
|
||||
**Traversal Order**
|
||||
@[inline] nonrec def ResolveT.run
|
||||
(ws : Workspace) (x : ResolveT m α) (stack : DepStack := {})
|
||||
: m (α × Workspace) :=
|
||||
x.run stack |>.run ws
|
||||
|
||||
All dependencies of a package are visited in order before recursing to the
|
||||
dependencies' dependencies. For example, given the dependency graph:
|
||||
|
||||
```
|
||||
R
|
||||
|- A
|
||||
|- B
|
||||
|- X
|
||||
|- Y
|
||||
|- C
|
||||
```
|
||||
|
||||
Lake follows the order `R`, `A`, `B`, `C`, `X`, `Y`.
|
||||
|
||||
The logic behind this design is that users would expect the dependencies
|
||||
they write in a package configuration to be resolved accordingly and would be
|
||||
surprised if they are overridden by nested dependencies referring to the same
|
||||
package.
|
||||
|
||||
For example, were Lake to use a pure depth-first traversal, Lake would follow
|
||||
the order `R`, `A`, `B`, `X`, `Y`, `C`. If `X` and `C` are both the package
|
||||
`foo`, Lake would use the configuration of `foo` found in `B` rather than in
|
||||
the root `R`, which would likely confuse the user.
|
||||
-/
|
||||
@[specialize] def Workspace.resolveDeps
|
||||
/-- Recursively run a `ResolveT` monad starting from the workspace's root. -/
|
||||
@[specialize] private def Workspace.runResolveT
|
||||
[Monad m] [MonadError m] (ws : Workspace)
|
||||
(breadth : Package → Dependency → ResolveT m Package)
|
||||
(depth : Package → m PUnit := fun _ => pure ())
|
||||
(go : RecFetchFn Package PUnit (ResolveT m))
|
||||
(root := ws.root) (stack : DepStack := {})
|
||||
: m Workspace := do
|
||||
let (root, ws) ← ResolveT.run ws <| StateT.run' (s := {}) <|
|
||||
inline <| recFetchAcyclic (·.name) go ws.root
|
||||
return {ws with root}
|
||||
let (_, ws) ← ResolveT.run ws (stack := stack) do
|
||||
inline <| recFetchAcyclic (·.name) go root
|
||||
return ws
|
||||
|
||||
/-
|
||||
Recursively visits each node in a package's dependency graph, starting from
|
||||
the workspace package `root`. Each dependency missing from the workspace is
|
||||
resolved using the `resolve` function and added into the workspace.
|
||||
|
||||
Recursion occurs breadth-first. Each direct dependency of a package is
|
||||
resolved in reverse order before recursing to the dependencies' dependencies.
|
||||
|
||||
See `Workspace.updateAndMaterializeCore` for more details.
|
||||
-/
|
||||
@[inline] private def Workspace.resolveDepsCore
|
||||
[Monad m] [MonadError m] (ws : Workspace)
|
||||
(load : Package → Dependency → StateT Workspace m Package)
|
||||
(root : Package := ws.root) (stack : DepStack := {})
|
||||
: m Workspace := do
|
||||
ws.runResolveT go root stack
|
||||
where
|
||||
@[specialize] go pkg resolve : StateT (NameMap Package) (ResolveT m) Package := do
|
||||
pkg.depConfigs.forM fun dep => do
|
||||
if (← getThe (NameMap Package)).contains dep.name then
|
||||
return
|
||||
if (← getThe Workspace).packageMap.contains dep.name then
|
||||
return -- already resolved in another branch
|
||||
@[specialize] go pkg recurse : ResolveT m Unit := do
|
||||
let start := (← getWorkspace).packages.size
|
||||
-- Materialize and load the missing direct dependencies of `pkg`
|
||||
pkg.depConfigs.forRevM fun dep => do
|
||||
let ws ← getWorkspace
|
||||
if ws.packageMap.contains dep.name then
|
||||
return -- already handled in another branch
|
||||
if pkg.name = dep.name then
|
||||
error s!"{pkg.name}: package requires itself (or a package with the same name)"
|
||||
let pre ← breadth pkg dep -- package w/o dependencies
|
||||
store dep.name pre
|
||||
let deps ← pkg.depConfigs.mapM fun dep => do
|
||||
if let some pre ← fetch? dep.name then
|
||||
modifyThe (NameMap Package) (·.erase dep.name) -- for `dep` linearity
|
||||
depth pre
|
||||
return OpaquePackage.mk (← resolve pre)
|
||||
if let some dep ← findPackage? dep.name then
|
||||
return OpaquePackage.mk dep -- already resolved in another branch
|
||||
error s!"{dep.name}: impossible resolution state reached"
|
||||
let pkg := {pkg with opaqueDeps := deps}
|
||||
modifyThe Workspace (·.addPackage pkg)
|
||||
return pkg
|
||||
|
||||
def stdMismatchError (newName : String) (rev : String) :=
|
||||
s!"the 'std' package has been renamed to '{newName}' and moved to the
|
||||
'leanprover-community' organization; downstream packages which wish to
|
||||
update to the new std should replace
|
||||
|
||||
require std from
|
||||
git \"https://github.com/leanprover/std4\"{rev}
|
||||
|
||||
in their Lake configuration file with
|
||||
|
||||
require {newName} from
|
||||
git \"https://github.com/leanprover-community/{newName}\"{rev}
|
||||
|
||||
"
|
||||
let depPkg ← load pkg dep
|
||||
modifyThe Workspace (·.addPackage depPkg)
|
||||
-- Recursively load the dependencies' dependencies
|
||||
(← getWorkspace).packages.forM recurse start
|
||||
|
||||
/--
|
||||
The monad of the manifest updater.
|
||||
It is equipped with and entry map entries for the updated manifest.
|
||||
Adds monad state used to update the manifest.
|
||||
It equips the monad with a map of locked dependencies.
|
||||
-/
|
||||
abbrev UpdateT := StateT (NameMap PackageEntry)
|
||||
|
||||
@@ -147,7 +144,9 @@ abbrev UpdateT := StateT (NameMap PackageEntry)
|
||||
Reuse manifest versions of root packages that should not be updated.
|
||||
Also, move the packages directory if its location has changed.
|
||||
-/
|
||||
def reuseManifest (ws : Workspace) (toUpdate : NameSet) : UpdateT LogIO PUnit := do
|
||||
private def reuseManifest
|
||||
(ws : Workspace) (toUpdate : NameSet)
|
||||
: UpdateT LogIO PUnit := do
|
||||
let rootName := ws.root.name.toString (escape := false)
|
||||
match (← Manifest.load ws.manifestFile |>.toBaseIO) with
|
||||
| .ok manifest =>
|
||||
@@ -175,7 +174,7 @@ def reuseManifest (ws : Workspace) (toUpdate : NameSet) : UpdateT LogIO PUnit :=
|
||||
logWarning s!"{rootName}: ignoring previous manifest because it failed to load: {e}"
|
||||
|
||||
/-- Add a package dependency's manifest entries to the update state. -/
|
||||
def addDependencyEntries (pkg : Package) : UpdateT LogIO PUnit := do
|
||||
private def addDependencyEntries (pkg : Package) : UpdateT LogIO PUnit := do
|
||||
match (← Manifest.load pkg.manifestFile |>.toBaseIO) with
|
||||
| .ok manifest =>
|
||||
manifest.packages.forM fun entry => do
|
||||
@@ -187,22 +186,31 @@ def addDependencyEntries (pkg : Package) : UpdateT LogIO PUnit := do
|
||||
| .error e =>
|
||||
logWarning s!"{pkg.name}: ignoring manifest because it failed to load: {e}"
|
||||
|
||||
/-- Update a single dependency. -/
|
||||
def updateDep
|
||||
(pkg : Package) (dep : Dependency) (leanOpts : Options := {})
|
||||
: ResolveT (UpdateT LogIO) Package := do
|
||||
let ws ← getThe Workspace
|
||||
let inherited := pkg.name != ws.root.name
|
||||
-- Materialize the dependency
|
||||
let matDep ← id do
|
||||
if let some entry ← fetch? dep.name then
|
||||
entry.materialize ws.lakeEnv ws.dir ws.relPkgsDir
|
||||
else
|
||||
let matDep ← dep.materialize inherited ws.lakeEnv ws.dir ws.relPkgsDir pkg.relDir
|
||||
store matDep.name matDep.manifestEntry
|
||||
return matDep
|
||||
-- Load the package
|
||||
let depPkg ← loadDepPackage matDep dep.opts leanOpts true
|
||||
/-- Materialize a single dependency, updating it if desired. -/
|
||||
private def updateAndMaterializeDep
|
||||
(ws : Workspace) (pkg : Package) (dep : Dependency)
|
||||
: UpdateT LogIO MaterializedDep := do
|
||||
if let some entry ← fetch? dep.name then
|
||||
entry.materialize ws.lakeEnv ws.dir ws.relPkgsDir
|
||||
else
|
||||
let inherited := pkg.name ≠ ws.root.name
|
||||
/-
|
||||
NOTE: A path dependency inherited from another dependency's manifest
|
||||
will always be of the form a `./<relPath>` (i.e., be relative to its
|
||||
workspace). Thus, when relativized to this workspace, it will have the
|
||||
path `<relPkgDir>/./<relPath>`. However, if defining dependency lacks
|
||||
a manifest, it will instead be locked as `<relPkgDir>/<relPath>`.
|
||||
Adding a `.` here eliminates this difference.
|
||||
-/
|
||||
let relPkgDir := if pkg.relDir == "." then pkg.relDir else pkg.relDir / "."
|
||||
let matDep ← dep.materialize inherited ws.lakeEnv ws.dir ws.relPkgsDir relPkgDir
|
||||
store matDep.name matDep.manifestEntry
|
||||
return matDep
|
||||
|
||||
/-- Verify that a dependency was loaded with the correct name. -/
|
||||
private def validateDep
|
||||
(pkg : Package) (dep : Dependency) (matDep : MaterializedDep) (depPkg : Package)
|
||||
: LogIO PUnit := do
|
||||
if depPkg.name ≠ dep.name then
|
||||
if dep.name = .mkSimple "std" then
|
||||
let rev :=
|
||||
@@ -216,24 +224,144 @@ def updateDep
|
||||
logError s!"'{dep.name}' was downloaded incorrectly; \
|
||||
you will need to manually delete '{depPkg.dir}': {e}"
|
||||
error s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
|
||||
return depPkg
|
||||
|
||||
/--
|
||||
Rebuild the workspace's Lake manifest and materialize missing dependencies.
|
||||
|
||||
Packages are updated to latest specific revision matching that in `require`
|
||||
(e.g., if the `require` is `@master`, update to latest commit on master) or
|
||||
removed if the `require` is removed. If `tuUpdate` is empty, update/remove all
|
||||
root dependencies. Otherwise, only update the root dependencies specified.
|
||||
|
||||
Package are always reconfigured when updated.
|
||||
Exit code returned if Lake needs a manual restart.
|
||||
Used, for instance, if the toolchain is updated and no Elan is detected.
|
||||
-/
|
||||
def Workspace.updateAndMaterialize
|
||||
(ws : Workspace) (toUpdate : NameSet := {}) (leanOpts : Options := {})
|
||||
: LogIO Workspace := do
|
||||
let (ws, entries) ← UpdateT.run do
|
||||
reuseManifest ws toUpdate
|
||||
ws.resolveDeps (updateDep · · leanOpts) (addDependencyEntries ·)
|
||||
def restartCode : ExitCode := 4
|
||||
|
||||
/--
|
||||
Update the workspace's `lean-toolchain` if necessary.
|
||||
|
||||
Compares the root's toolchain with that of its direct dependencies to find the
|
||||
best match. If none can be found, issue warning and return normally. If an
|
||||
update is found
|
||||
-/
|
||||
def Workspace.updateToolchain
|
||||
(ws : Workspace) (rootDeps : Array MaterializedDep)
|
||||
: LoggerIO PUnit := do
|
||||
let rootToolchainFile := ws.root.dir / toolchainFileName
|
||||
let rootTc? ← ToolchainVer.ofDir? ws.dir
|
||||
let (src, tc?, tcs) ← rootDeps.foldlM (init := (ws.root.name, rootTc?, #[])) fun s dep => do
|
||||
let depTc? ← ToolchainVer.ofDir? (ws.dir / dep.relPkgDir)
|
||||
let some depTc := depTc?
|
||||
| return s
|
||||
let (src, tc?, tcs) := s
|
||||
let some tc := tc?
|
||||
| return (dep.name, depTc?, tcs)
|
||||
if depTc ≤ tc then
|
||||
return (src, tc, tcs)
|
||||
else if tc < depTc then
|
||||
return (dep.name, depTc, tcs)
|
||||
else
|
||||
return (src, tc, tcs.push (dep.name, depTc))
|
||||
if 0 < tcs.size then
|
||||
let s := "toolchain not updated; multiple toolchain candidates:"
|
||||
let s := if let some tc := tc? then s!"{s}\n {tc}\n from {src}" else s
|
||||
let s := tcs.foldl (init := s) fun s (d, tc) => s!"{s}\n {tc}\n from {d}"
|
||||
logWarning s
|
||||
else if let some tc := tc? then
|
||||
if rootTc?.any (· == tc) then
|
||||
logInfo "toolchain not updated; already up-to-date"
|
||||
return
|
||||
logInfo s!"updating toolchain to '{tc}'"
|
||||
IO.FS.writeFile rootToolchainFile tc.toString
|
||||
let some lakeArgs := ws.lakeArgs?
|
||||
| logInfo s!"cannot auto-restart; you will need to manually restart Lake"
|
||||
IO.Process.exit restartCode.toUInt8
|
||||
let some elanInstall := ws.lakeEnv.elan?
|
||||
| logInfo s!"no Elan detected; you will need to manually restart Lake"
|
||||
IO.Process.exit restartCode.toUInt8
|
||||
logInfo s!"restarting Lake via Elan"
|
||||
let child ← IO.Process.spawn {
|
||||
cmd := elanInstall.elan.toString
|
||||
args := #["run", "--install", tc.toString, "lake"] ++ lakeArgs
|
||||
env := Env.noToolchainVars
|
||||
}
|
||||
IO.Process.exit (← child.wait).toUInt8
|
||||
else
|
||||
logInfo s!"toolchain not updated; no toolchain information found"
|
||||
|
||||
/--
|
||||
Updates the workspace, materializing and reconfiguring dependencies.
|
||||
|
||||
Dependencies are updated to latest specific revision matching that in `require`
|
||||
(e.g., if the `require` is `@master`, update to latest commit on master) or
|
||||
removed if the `require` is removed.
|
||||
If `tuUpdate` is empty, all direct dependencies of the workspace's root will be
|
||||
updated and/or remove. Otherwise, only those specified will be updated.
|
||||
|
||||
If `updateToolchain := true`, the workspace's toolchain is also updated to the
|
||||
latest toolchain compatible with the root and its direct dependencies.
|
||||
If there are multiple incomparable toolchain versions across them,
|
||||
a warning will be issued and no update performed.
|
||||
If an update is performed, Lake will automatically restart the update on the new
|
||||
toolchain (via `elan`). If `elan` is missing, it will instead request a manual
|
||||
restart from the user and exit immediately with `restartCode`.
|
||||
|
||||
**Dependency Traversal Order**
|
||||
|
||||
All dependencies of a package are visited in reverse order before recursing
|
||||
to the dependencies' dependencies. For example, given the dependency graph:
|
||||
|
||||
```
|
||||
R
|
||||
|- A
|
||||
|- B
|
||||
|- X
|
||||
|- Y
|
||||
|- C
|
||||
```
|
||||
|
||||
Lake follows the order `R`, `C`, `A`, `B`, `Y`, `X`.
|
||||
|
||||
The reason for this is two-fold:
|
||||
1. Like targets, later requires should shadow earlier definitions.
|
||||
2. Requires written by a user should take priority over those inherited
|
||||
from dependencies.
|
||||
|
||||
Were Lake to use a depth-first traversal, for example, Lake would follow
|
||||
the order `R`, `A`, `B`, `X`, `Y`, `C`. If `X` and `C` are both the package
|
||||
`foo`, Lake would use the configuration of `foo` found in `B` rather than in
|
||||
the root `R`, which would likely confuse the user.
|
||||
-/
|
||||
def Workspace.updateAndMaterializeCore
|
||||
(ws : Workspace)
|
||||
(toUpdate : NameSet := {}) (leanOpts : Options := {})
|
||||
(updateToolchain := true)
|
||||
: LoggerIO (Workspace × NameMap PackageEntry) := UpdateT.run do
|
||||
reuseManifest ws toUpdate
|
||||
let ws := ws.addPackage ws.root
|
||||
if updateToolchain then
|
||||
let deps := ws.root.depConfigs.reverse
|
||||
let matDeps ← deps.mapM fun dep => do
|
||||
logVerbose s!"{ws.root.name}: updating '{dep.name}' with {toJson dep.opts}"
|
||||
updateAndMaterializeDep ws ws.root dep
|
||||
ws.updateToolchain matDeps
|
||||
let start := ws.packages.size
|
||||
let ws ← (deps.zip matDeps).foldlM (init := ws) fun ws (dep, matDep) => do
|
||||
let (depPkg, ws) ← loadUpdatedDep ws.root dep matDep ws
|
||||
let ws := ws.addPackage depPkg
|
||||
return ws
|
||||
ws.packages.foldlM (init := ws) (start := start) fun ws pkg =>
|
||||
ws.resolveDepsCore (stack := [ws.root.name]) updateAndLoadDep pkg
|
||||
else
|
||||
ws.resolveDepsCore updateAndLoadDep
|
||||
where
|
||||
@[inline] updateAndLoadDep pkg dep := do
|
||||
let matDep ← updateAndMaterializeDep (← getWorkspace) pkg dep
|
||||
loadUpdatedDep pkg dep matDep
|
||||
@[inline] loadUpdatedDep pkg dep matDep : StateT Workspace (UpdateT LogIO) Package := do
|
||||
let depPkg ← loadDepPackage matDep dep.opts leanOpts true
|
||||
validateDep pkg dep matDep depPkg
|
||||
addDependencyEntries depPkg
|
||||
return depPkg
|
||||
|
||||
/-- Write package entries to the workspace manifest. -/
|
||||
def Workspace.writeManifest
|
||||
(ws : Workspace) (entries : NameMap PackageEntry)
|
||||
: LogIO PUnit := do
|
||||
let manifestEntries := ws.packages.foldl (init := #[]) fun arr pkg =>
|
||||
match entries.find? pkg.name with
|
||||
| some entry => arr.push <|
|
||||
@@ -246,10 +374,28 @@ def Workspace.updateAndMaterialize
|
||||
packages := manifestEntries
|
||||
}
|
||||
manifest.saveToFile ws.manifestFile
|
||||
LakeT.run ⟨ws⟩ <| ws.packages.forM fun pkg => do
|
||||
unless pkg.postUpdateHooks.isEmpty do
|
||||
logInfo s!"{pkg.name}: running post-update hooks"
|
||||
pkg.postUpdateHooks.forM fun hook => hook.get.fn pkg
|
||||
|
||||
/-- Run a package's `post_update` hooks. -/
|
||||
def Package.runPostUpdateHooks (pkg : Package) : LakeT LogIO PUnit := do
|
||||
unless pkg.postUpdateHooks.isEmpty do
|
||||
logInfo s!"{pkg.name}: running post-update hooks"
|
||||
pkg.postUpdateHooks.forM fun hook => hook.get.fn pkg
|
||||
|
||||
/--
|
||||
Updates the workspace, writes the new Lake manifest, and runs package
|
||||
post-update hooks.
|
||||
|
||||
See `Workspace.updateAndMaterializeCore` for details on the update process.
|
||||
-/
|
||||
def Workspace.updateAndMaterialize
|
||||
(ws : Workspace)
|
||||
(toUpdate : NameSet := {}) (leanOpts : Options := {})
|
||||
(updateToolchain := true)
|
||||
: LoggerIO Workspace := do
|
||||
let (ws, entries) ←
|
||||
ws.updateAndMaterializeCore toUpdate leanOpts updateToolchain
|
||||
ws.writeManifest entries
|
||||
ws.runLakeT do ws.packages.forM (·.runPostUpdateHooks)
|
||||
return ws
|
||||
|
||||
/--
|
||||
@@ -293,8 +439,9 @@ def Workspace.materializeDeps
|
||||
let pkgEntries : NameMap PackageEntry := manifest.packages.foldl (init := {})
|
||||
fun map entry => map.insert entry.name entry
|
||||
validateManifest pkgEntries ws.root.depConfigs
|
||||
ws.resolveDeps fun pkg dep => do
|
||||
let ws ← getThe Workspace
|
||||
let ws := ws.addPackage ws.root
|
||||
ws.resolveDepsCore fun pkg dep => do
|
||||
let ws ← getWorkspace
|
||||
if let some entry := pkgEntries.find? dep.name then
|
||||
let result ← entry.materialize ws.lakeEnv ws.dir relPkgsDir
|
||||
loadDepPackage result dep.opts leanOpts reconfigure
|
||||
|
||||
@@ -25,7 +25,9 @@ def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
|
||||
Lean.searchPathRef.set config.lakeEnv.leanSearchPath
|
||||
let (root, env?) ← loadPackageCore "[root]" config
|
||||
let ws : Workspace := {
|
||||
root, lakeEnv := config.lakeEnv
|
||||
root
|
||||
lakeEnv := config.lakeEnv
|
||||
lakeArgs? := config.lakeArgs?
|
||||
moduleFacetConfigs := initModuleFacetConfigs
|
||||
packageFacetConfigs := initPackageFacetConfigs
|
||||
libraryFacetConfigs := initLibraryFacetConfigs
|
||||
@@ -40,19 +42,19 @@ Load a `Workspace` for a Lake package by
|
||||
elaborating its configuration file and resolving its dependencies.
|
||||
If `updateDeps` is true, updates the manifest before resolving dependencies.
|
||||
-/
|
||||
def loadWorkspace (config : LoadConfig) (updateDeps := false) : LogIO Workspace := do
|
||||
let rc := config.reconfigure
|
||||
let leanOpts := config.leanOpts
|
||||
def loadWorkspace (config : LoadConfig) : LoggerIO Workspace := do
|
||||
let {reconfigure, leanOpts, updateDeps, updateToolchain, ..} := config
|
||||
let ws ← loadWorkspaceRoot config
|
||||
if updateDeps then
|
||||
ws.updateAndMaterialize {} leanOpts
|
||||
ws.updateAndMaterialize {} leanOpts updateToolchain
|
||||
else if let some manifest ← Manifest.load? ws.manifestFile then
|
||||
ws.materializeDeps manifest leanOpts rc
|
||||
ws.materializeDeps manifest leanOpts reconfigure
|
||||
else
|
||||
ws.updateAndMaterialize {} leanOpts
|
||||
ws.updateAndMaterialize {} leanOpts updateToolchain
|
||||
|
||||
/-- Updates the manifest for the loaded Lake workspace (see `updateAndMaterialize`). -/
|
||||
def updateManifest (config : LoadConfig) (toUpdate : NameSet := {}) : LogIO Unit := do
|
||||
let leanOpts := config.leanOpts
|
||||
def updateManifest (config : LoadConfig) (toUpdate : NameSet := {})
|
||||
: LoggerIO Unit := do
|
||||
let {leanOpts, updateToolchain, ..} := config
|
||||
let ws ← loadWorkspaceRoot config
|
||||
discard <| ws.updateAndMaterialize toUpdate leanOpts
|
||||
discard <| ws.updateAndMaterialize toUpdate leanOpts updateToolchain
|
||||
|
||||
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Util.Date
|
||||
|
||||
/-!
|
||||
# TOML Date-Time
|
||||
@@ -22,62 +23,10 @@ optionally left out, creating four distinct variants.
|
||||
|
||||
namespace Lake.Toml
|
||||
|
||||
def lpad (s : String) (c : Char) (len : Nat) : String :=
|
||||
"".pushn c (len - s.length) ++ s
|
||||
|
||||
def rpad (s : String) (c : Char) (len : Nat) : String :=
|
||||
s.pushn c (len - s.length)
|
||||
|
||||
def zpad (n : Nat) (len : Nat) : String :=
|
||||
lpad (toString n) '0' len
|
||||
|
||||
/-- A TOML date (year-month-day). -/
|
||||
structure Date where
|
||||
year : Nat
|
||||
month : Nat
|
||||
day : Nat
|
||||
deriving Inhabited, DecidableEq, Ord
|
||||
|
||||
namespace Date
|
||||
|
||||
abbrev IsLeapYear (y : Nat) : Prop :=
|
||||
y % 4 = 0 ∧ (y % 100 ≠ 0 ∨ y % 400 = 0)
|
||||
|
||||
abbrev IsValidMonth (m : Nat) : Prop :=
|
||||
m ≥ 1 ∧ m ≤ 12
|
||||
|
||||
def maxDay (y m : Nat) : Nat :=
|
||||
if m = 2 then
|
||||
if IsLeapYear y then 29 else 28
|
||||
else if m ≤ 7 then
|
||||
30 + (m % 2)
|
||||
else
|
||||
31 - (m % 2)
|
||||
|
||||
abbrev IsValidDay (y m d : Nat) : Prop :=
|
||||
d ≥ 1 ∧ d ≤ maxDay y m
|
||||
|
||||
def ofValid? (year month day : Nat) : Option Date := do
|
||||
guard (IsValidMonth month ∧ IsValidDay year month day)
|
||||
return {year, month, day}
|
||||
|
||||
def ofString? (t : String) : Option Date := do
|
||||
match t.split (· == '-') with
|
||||
| [y,m,d] =>
|
||||
ofValid? (← y.toNat?) (← m.toNat?) (← d.toNat?)
|
||||
| _ => none
|
||||
|
||||
protected def toString (d : Date) : String :=
|
||||
s!"{zpad d.year 4}-{zpad d.month 2}-{zpad d.day 2}"
|
||||
|
||||
instance : ToString Date := ⟨Date.toString⟩
|
||||
|
||||
end Date
|
||||
|
||||
/--
|
||||
A TOML time (hour:minute:second.fraction).
|
||||
|
||||
We do not represent whole time as seconds to due to the possibility
|
||||
We do not represent the whole time as seconds to due to the possibility
|
||||
of leap seconds in RFC 3339 times.
|
||||
-/
|
||||
structure Time where
|
||||
|
||||
69
src/lake/Lake/Util/Date.lean
Normal file
69
src/lake/Lake/Util/Date.lean
Normal file
@@ -0,0 +1,69 @@
|
||||
/-
|
||||
Copyright (c) 2024 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
|
||||
/-!
|
||||
# Date
|
||||
|
||||
A year-mont-day date. Used by Lake's TOML parser and its toolchain version
|
||||
parser (for nightlies).
|
||||
-/
|
||||
|
||||
namespace Lake
|
||||
|
||||
def lpad (s : String) (c : Char) (len : Nat) : String :=
|
||||
"".pushn c (len - s.length) ++ s
|
||||
|
||||
def rpad (s : String) (c : Char) (len : Nat) : String :=
|
||||
s.pushn c (len - s.length)
|
||||
|
||||
def zpad (n : Nat) (len : Nat) : String :=
|
||||
lpad (toString n) '0' len
|
||||
|
||||
/-- A date (year-month-day). -/
|
||||
structure Date where
|
||||
year : Nat
|
||||
month : Nat
|
||||
day : Nat
|
||||
deriving Inhabited, DecidableEq, Ord, Repr
|
||||
|
||||
namespace Date
|
||||
|
||||
instance : LT Date := ltOfOrd
|
||||
instance : LE Date := leOfOrd
|
||||
instance : Min Date := minOfLe
|
||||
instance : Max Date := maxOfLe
|
||||
|
||||
abbrev IsLeapYear (y : Nat) : Prop :=
|
||||
y % 4 = 0 ∧ (y % 100 ≠ 0 ∨ y % 400 = 0)
|
||||
|
||||
abbrev IsValidMonth (m : Nat) : Prop :=
|
||||
m ≥ 1 ∧ m ≤ 12
|
||||
|
||||
def maxDay (y m : Nat) : Nat :=
|
||||
if m = 2 then
|
||||
if IsLeapYear y then 29 else 28
|
||||
else if m ≤ 7 then
|
||||
30 + (m % 2)
|
||||
else
|
||||
31 - (m % 2)
|
||||
|
||||
abbrev IsValidDay (y m d : Nat) : Prop :=
|
||||
d ≥ 1 ∧ d ≤ maxDay y m
|
||||
|
||||
def ofValid? (year month day : Nat) : Option Date := do
|
||||
guard (IsValidMonth month ∧ IsValidDay year month day)
|
||||
return {year, month, day}
|
||||
|
||||
def ofString? (t : String) : Option Date := do
|
||||
match t.split (· == '-') with
|
||||
| [y,m,d] =>
|
||||
ofValid? (← y.toNat?) (← m.toNat?) (← d.toNat?)
|
||||
| _ => none
|
||||
|
||||
protected def toString (d : Date) : String :=
|
||||
s!"{zpad d.year 4}-{zpad d.month 2}-{zpad d.day 2}"
|
||||
|
||||
instance : ToString Date := ⟨Date.toString⟩
|
||||
@@ -5,33 +5,39 @@ Authors: Mac Malone
|
||||
-/
|
||||
namespace Lake
|
||||
|
||||
instance (priority := low) [Monad m] [MonadExceptOf PUnit m] : Alternative m where
|
||||
failure := throw ()
|
||||
orElse := tryCatch
|
||||
|
||||
/-- Ensure direct lifts are preferred over indirect ones. -/
|
||||
instance (priority := high) [MonadLift α β] : MonadLiftT α β := ⟨MonadLift.monadLift⟩
|
||||
|
||||
instance [Pure m] : MonadLiftT Id m where
|
||||
instance (priority := low) [Pure m] : MonadLiftT Id m where
|
||||
monadLift act := pure act.run
|
||||
|
||||
instance [Alternative m] : MonadLiftT Option m where
|
||||
instance (priority := low) [Alternative m] : MonadLiftT Option m where
|
||||
monadLift
|
||||
| some a => pure a
|
||||
| none => failure
|
||||
|
||||
instance [Pure m] [MonadExceptOf ε m] : MonadLiftT (Except ε) m where
|
||||
instance (priority := low) [Pure m] [MonadExceptOf ε m] : MonadLiftT (Except ε) m where
|
||||
monadLift
|
||||
| .ok a => pure a
|
||||
| .error e => throw e
|
||||
|
||||
instance [Bind m] [MonadReaderOf ρ m] [MonadLiftT n m] : MonadLiftT (ReaderT ρ n) m where
|
||||
-- Remark: not necessarily optimal; uses context non-linearly
|
||||
instance (priority := low) [Bind m] [MonadReaderOf ρ m] [MonadLiftT n m] : MonadLiftT (ReaderT ρ n) m where
|
||||
monadLift act := do act (← read)
|
||||
|
||||
instance [Monad m] [MonadStateOf σ m] [MonadLiftT n m] : MonadLiftT (StateT σ n) m where
|
||||
-- Remark: not necessarily optimal; uses state non-linearly
|
||||
instance (priority := low) [Monad m] [MonadStateOf σ m] [MonadLiftT n m] : MonadLiftT (StateT σ n) m where
|
||||
monadLift act := do let (a, s) ← act (← get); set s; pure a
|
||||
|
||||
instance [Monad m] [Alternative m] [MonadLiftT n m] : MonadLiftT (OptionT n) m where
|
||||
instance (priority := low) [Monad m] [Alternative m] [MonadLiftT n m] : MonadLiftT (OptionT n) m where
|
||||
monadLift act := act.run >>= liftM
|
||||
|
||||
instance [Monad m] [MonadExceptOf ε m] [MonadLiftT n m] : MonadLiftT (ExceptT ε n) m where
|
||||
instance (priority := low) [Monad m] [MonadExceptOf ε m] [MonadLiftT n m] : MonadLiftT (ExceptT ε n) m where
|
||||
monadLift act := act.run >>= liftM
|
||||
|
||||
instance [Monad m] [MonadExceptOf ε m] [MonadLiftT BaseIO m] : MonadLiftT (EIO ε) m where
|
||||
instance (priority := low) [Monad m] [MonadExceptOf ε m] [MonadLiftT BaseIO m] : MonadLiftT (EIO ε) m where
|
||||
monadLift act := act.toBaseIO >>= liftM
|
||||
|
||||
@@ -5,6 +5,7 @@ Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Util.Error
|
||||
import Lake.Util.EStateT
|
||||
import Lake.Util.Lift
|
||||
import Lean.Data.Json
|
||||
import Lean.Message
|
||||
|
||||
@@ -195,6 +196,9 @@ abbrev stream [MonadLiftT BaseIO m]
|
||||
(out : IO.FS.Stream) (minLv := LogLevel.info) (useAnsi := false)
|
||||
: MonadLog m where logEntry e := logToStream e out minLv useAnsi
|
||||
|
||||
@[inline] def error [Alternative m] [MonadLog m] (msg : String) : m α :=
|
||||
logError msg *> failure
|
||||
|
||||
end MonadLog
|
||||
|
||||
def OutStream.logEntry
|
||||
@@ -404,7 +408,7 @@ from an `ELogT` (e.g., `LogIO`).
|
||||
(msg : String)
|
||||
: m α := errorWithLog (logError msg)
|
||||
|
||||
/-- `Alternative` instance for monads with `Log` state and `Log.Pos` errors. -/
|
||||
/-- `MonadError` instance for monads with `Log` state and `Log.Pos` errors. -/
|
||||
abbrev ELog.monadError
|
||||
[Monad m] [MonadLog m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m]
|
||||
: MonadError m := ⟨ELog.error⟩
|
||||
@@ -505,7 +509,7 @@ abbrev run?' [Functor m] (self : ELogT m α) (log : Log := {}) : m (Option α) :
|
||||
Run `self` with the log taken from the state of the monad `n`,
|
||||
|
||||
**Warning:** If lifting `self` from `m` to `n` fails, the log will be lost.
|
||||
Thus, this is best used when the lift cannot fail. Note excludes the
|
||||
Thus, this is best used when the lift cannot fail. This excludes the
|
||||
native log position failure of `ELogT`, which are lifted safely.
|
||||
-/
|
||||
@[inline] def takeAndRun
|
||||
@@ -545,8 +549,6 @@ instance : MonadLift IO LogIO := ⟨MonadError.runIO⟩
|
||||
|
||||
namespace LogIO
|
||||
|
||||
@[deprecated ELogT.run? (since := "2024-05-18")] abbrev captureLog := @ELogT.run?
|
||||
|
||||
/--
|
||||
Runs a `LogIO` action in `BaseIO`.
|
||||
Prints log entries of at least `minLv` to `out`.
|
||||
@@ -563,4 +565,46 @@ where
|
||||
replay (log : Log) (logger : MonadLog BaseIO) : BaseIO Unit :=
|
||||
log.replay (logger := logger)
|
||||
|
||||
-- deprecated 2024-05-18, reversed 2024-10-18
|
||||
abbrev captureLog := @ELogT.run?
|
||||
|
||||
end LogIO
|
||||
|
||||
/--
|
||||
A monad equipped with a log function and the ability to perform I/O.
|
||||
Unlike `LogIO`, log entries are not retained by the monad but instead eagerly
|
||||
passed to the log function.
|
||||
-/
|
||||
abbrev LoggerIO := MonadLogT BaseIO (EIO PUnit)
|
||||
|
||||
instance : MonadError LoggerIO := ⟨MonadLog.error⟩
|
||||
instance : MonadLift IO LoggerIO := ⟨MonadError.runIO⟩
|
||||
instance : MonadLift LogIO LoggerIO := ⟨ELogT.replayLog⟩
|
||||
|
||||
namespace LoggerIO
|
||||
|
||||
/--
|
||||
Runs a `LoggerIO` action in `BaseIO`.
|
||||
Prints log entries of at least `minLv` to `out`.
|
||||
-/
|
||||
@[inline] def toBaseIO
|
||||
(self : LoggerIO α)
|
||||
(minLv := LogLevel.info) (ansiMode := AnsiMode.auto) (out := OutStream.stderr)
|
||||
: BaseIO (Option α) := do
|
||||
(·.toOption) <$> (self.run (← out.getLogger minLv ansiMode)).toBaseIO
|
||||
|
||||
def captureLog (self : LoggerIO α) : BaseIO (Option α × Log) := do
|
||||
let ref ← IO.mkRef ({} : Log)
|
||||
let e ← self.run ⟨fun e => ref.modify (·.push e)⟩ |>.toBaseIO
|
||||
return (e.toOption, ← ref.get)
|
||||
|
||||
-- For parity with `LogIO.run?`
|
||||
abbrev run? := @captureLog
|
||||
|
||||
-- For parity with `LogIO.run?'`
|
||||
@[inline] def run?'
|
||||
(self : LoggerIO α) (logger : LogEntry → BaseIO PUnit := fun _ => pure ())
|
||||
: BaseIO (Option α) := do
|
||||
(·.toOption) <$> (self.run ⟨logger⟩).toBaseIO
|
||||
|
||||
end LoggerIO
|
||||
|
||||
@@ -88,3 +88,12 @@ where
|
||||
log.replay (logger := logger)
|
||||
|
||||
instance (priority := low) : MonadLift LogIO MainM := ⟨runLogIO⟩
|
||||
|
||||
@[inline] def runLoggerIO (x : LoggerIO α)
|
||||
(minLv := LogLevel.info) (ansiMode := AnsiMode.auto) (out := OutStream.stderr)
|
||||
: MainM α := do
|
||||
let some a ← x.run (← out.getLogger minLv ansiMode) |>.toBaseIO
|
||||
| exit 1
|
||||
return a
|
||||
|
||||
instance (priority := low) : MonadLift LoggerIO MainM := ⟨runLoggerIO⟩
|
||||
|
||||
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lean.Elab.Eval
|
||||
import Lake.Util.Date
|
||||
|
||||
/-! # Version
|
||||
|
||||
@@ -11,7 +12,7 @@ This module contains useful definitions for manipulating versions.
|
||||
It also defines a `v!"<ver>"` syntax for version literals.
|
||||
-/
|
||||
|
||||
open Lean
|
||||
open System Lean
|
||||
|
||||
namespace Lake
|
||||
|
||||
@@ -117,6 +118,112 @@ instance : ToExpr StdVer where
|
||||
#[toExpr ver.toSemVerCore, toExpr ver.specialDescr]
|
||||
toTypeExpr := mkConst ``StdVer
|
||||
|
||||
/-- A Lean toolchain version. -/
|
||||
inductive ToolchainVer
|
||||
| release (ver : LeanVer)
|
||||
| nightly (date : Date)
|
||||
| pr (no : Nat)
|
||||
| other (name : String)
|
||||
deriving Repr, DecidableEq
|
||||
|
||||
instance : Coe LeanVer ToolchainVer := ⟨ToolchainVer.release⟩
|
||||
|
||||
def ToolchainVer.defaultOrigin := "leanprover/lean4"
|
||||
def ToolchainVer.prOrigin := "leanprover/lean4-pr-releases"
|
||||
|
||||
def ToolchainVer.ofString (ver : String) : ToolchainVer := Id.run do
|
||||
let colonPos := ver.posOf ':'
|
||||
let (origin, tag) :=
|
||||
if h : colonPos < ver.endPos then
|
||||
let pos := ver.next' colonPos (by simp_all [h, String.endPos, String.atEnd])
|
||||
(ver.extract 0 colonPos, ver.extract pos ver.endPos)
|
||||
else
|
||||
("", ver)
|
||||
if tag.startsWith "v" then
|
||||
if let .ok ver := StdVer.parse (tag.drop 1) then
|
||||
if origin.isEmpty || origin == defaultOrigin then
|
||||
return .release ver
|
||||
return .other ver
|
||||
else if tag.startsWith "nightly-" then
|
||||
if let some date := Date.ofString? (tag.drop "nightly-".length) then
|
||||
if origin.isEmpty || origin == defaultOrigin then
|
||||
return .nightly date
|
||||
else if tag.startsWith "pr-release-" then
|
||||
if let some n := (tag.drop "pr-release-".length).toNat? then
|
||||
if origin.isEmpty || origin == prOrigin then
|
||||
return .pr n
|
||||
else
|
||||
if let .ok ver := StdVer.parse ver then
|
||||
if origin.isEmpty || origin == defaultOrigin then
|
||||
return .release ver
|
||||
return .other ver
|
||||
|
||||
/-- Parse a toolchain from a `lean-toolchain` file. -/
|
||||
def ToolchainVer.ofFile? (toolchainFile : FilePath) : IO (Option ToolchainVer) := do
|
||||
try
|
||||
let toolchainString ← IO.FS.readFile toolchainFile
|
||||
return some <| ToolchainVer.ofString toolchainString.trim
|
||||
catch
|
||||
| .noFileOrDirectory .. =>
|
||||
return none
|
||||
| e => throw e
|
||||
|
||||
/-- The `elan` toolchain file name (i.e., `lean-toolchain`). -/
|
||||
def toolchainFileName : FilePath := "lean-toolchain"
|
||||
|
||||
/-- Parse a toolchain from the `lean-toolchain` file of the directory `dir`. -/
|
||||
@[inline] def ToolchainVer.ofDir? (dir : FilePath) : IO (Option ToolchainVer) :=
|
||||
ToolchainVer.ofFile? (dir / toolchainFileName)
|
||||
|
||||
protected def ToolchainVer.toString (ver : ToolchainVer) : String :=
|
||||
match ver with
|
||||
| .release ver => s!"{defaultOrigin}:v{ver}"
|
||||
| .nightly date => s!"{defaultOrigin}:nightly-{date}"
|
||||
| .pr n => s!"{prOrigin}:pr-release-{n}"
|
||||
| .other s => s
|
||||
|
||||
instance : ToString ToolchainVer := ⟨ToolchainVer.toString⟩
|
||||
instance : ToJson ToolchainVer := ⟨(·.toString)⟩
|
||||
instance : FromJson ToolchainVer := ⟨(ToolchainVer.ofString <$> fromJson? ·)⟩
|
||||
|
||||
protected def ToolchainVer.lt (a b : ToolchainVer) : Prop :=
|
||||
match a, b with
|
||||
| .release v1, .release v2 => v1 < v2
|
||||
| .nightly d1, .nightly d2 => d1 < d2
|
||||
| _, _ => False
|
||||
|
||||
instance : LT ToolchainVer := ⟨ToolchainVer.lt⟩
|
||||
|
||||
instance ToolchainVer.decLt (a b : ToolchainVer) : Decidable (a < b) :=
|
||||
match a, b with
|
||||
| .release v1, .release v2 => inferInstanceAs (Decidable (v1 < v2))
|
||||
| .nightly d1, .nightly d2 => inferInstanceAs (Decidable (d1 < d2))
|
||||
| .release _, .pr _ | .release _, .nightly _ | .release _, .other _
|
||||
| .nightly _, .release _ | .nightly _, .pr _ | .nightly _, .other _
|
||||
| .pr _, _ | .other _, _ => .isFalse (by simp [LT.lt, ToolchainVer.lt])
|
||||
|
||||
protected def ToolchainVer.le (a b : ToolchainVer) : Prop :=
|
||||
match a, b with
|
||||
| .release v1, .release v2 => v1 ≤ v2
|
||||
| .nightly d1, .nightly d2 => d1 ≤ d2
|
||||
| .pr n1, .pr n2 => n1 = n2
|
||||
| .other v1, .other v2 => v1 = v2
|
||||
| _, _ => False
|
||||
|
||||
instance : LE ToolchainVer := ⟨ToolchainVer.le⟩
|
||||
|
||||
instance ToolchainVer.decLe (a b : ToolchainVer) : Decidable (a ≤ b) :=
|
||||
match a, b with
|
||||
| .release v1, .release v2 => inferInstanceAs (Decidable (v1 ≤ v2))
|
||||
| .nightly d1, .nightly d2 => inferInstanceAs (Decidable (d1 ≤ d2))
|
||||
| .pr n1, .pr n2 => inferInstanceAs (Decidable (n1 = n2))
|
||||
| .other v1, .other v2 => inferInstanceAs (Decidable (v1 = v2))
|
||||
| .release _, .pr _ | .release _, .nightly _ | .release _, .other _
|
||||
| .nightly _, .release _ | .nightly _, .pr _ | .nightly _, other _
|
||||
| .pr _, .release _ | .pr _, .nightly _ | .pr _, .other _
|
||||
| .other _, .release _ | .other _, .nightly _ | .other _, .pr _ =>
|
||||
.isFalse (by simp [LE.le, ToolchainVer.le])
|
||||
|
||||
/-! ## Version Literals
|
||||
|
||||
Defines the `v!"<ver>"` syntax for version literals.
|
||||
@@ -134,6 +241,7 @@ export DecodeVersion (decodeVersion)
|
||||
|
||||
instance : DecodeVersion SemVerCore := ⟨SemVerCore.parse⟩
|
||||
@[default_instance] instance : DecodeVersion StdVer := ⟨StdVer.parse⟩
|
||||
instance : DecodeVersion ToolchainVer := ⟨(pure <| ToolchainVer.ofString ·)⟩
|
||||
|
||||
private def toResultExpr [ToExpr α] (x : Except String α) : Except String Expr :=
|
||||
Functor.map toExpr x
|
||||
|
||||
@@ -3,31 +3,31 @@
|
||||
"packages":
|
||||
[{"type": "path",
|
||||
"scope": "",
|
||||
"name": "root",
|
||||
"name": "foo",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inherited": true,
|
||||
"dir": "./../foo/../a/../root",
|
||||
"configFile": "lakefile.lean"},
|
||||
{"type": "path",
|
||||
"scope": "",
|
||||
"name": "a",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inherited": true,
|
||||
"dir": "./../foo/../a",
|
||||
"inherited": false,
|
||||
"dir": "./../foo",
|
||||
"configFile": "lakefile.lean"},
|
||||
{"type": "path",
|
||||
"scope": "",
|
||||
"name": "b",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inherited": true,
|
||||
"dir": "./../foo/../b",
|
||||
"dir": "./../foo/./../b",
|
||||
"configFile": "lakefile.lean"},
|
||||
{"type": "path",
|
||||
"scope": "",
|
||||
"name": "foo",
|
||||
"name": "a",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inherited": false,
|
||||
"dir": "./../foo",
|
||||
"inherited": true,
|
||||
"dir": "./../foo/./../a",
|
||||
"configFile": "lakefile.lean"},
|
||||
{"type": "path",
|
||||
"scope": "",
|
||||
"name": "root",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inherited": true,
|
||||
"dir": "./../foo/./../b/./../root",
|
||||
"configFile": "lakefile.lean"}],
|
||||
"name": "bar",
|
||||
"lakeDir": ".lake"}
|
||||
|
||||
@@ -1,6 +1,6 @@
|
||||
dep/hello
|
||||
scripts/say-goodbye
|
||||
scripts/greet
|
||||
dep/hello
|
||||
Hello, world!
|
||||
Hello, me!
|
||||
Hello, --me!
|
||||
@@ -16,8 +16,8 @@ Hello from Dep!
|
||||
Goodbye!
|
||||
error: unknown script nonexistent
|
||||
error: unknown script nonexistent
|
||||
dep/hello
|
||||
scripts/say-goodbye
|
||||
scripts/greet
|
||||
dep/hello
|
||||
Hello, world!
|
||||
Goodbye!
|
||||
|
||||
@@ -17,6 +17,7 @@ fi
|
||||
mkdir hello
|
||||
pushd hello
|
||||
$LAKE init hello
|
||||
rm -f lean-toolchain
|
||||
$LAKE update
|
||||
git init
|
||||
git checkout -b master
|
||||
@@ -34,7 +35,7 @@ cd test
|
||||
LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update 2>&1 | grep --color "file://"
|
||||
# test that a second `lake update` is a no-op (with URLs)
|
||||
# see https://github.com/leanprover/lean4/commit/6176fdba9e5a888225a23e5d558a005e0d1eb2f6#r125905901
|
||||
LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update 2>&1 | diff - /dev/null
|
||||
LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update --keep-toolchain 2>&1 | diff - /dev/null
|
||||
rm -rf .lake/packages
|
||||
|
||||
# Test that Lake produces no warnings on a `lake build` after a `lake update`
|
||||
@@ -42,7 +43,7 @@ rm -rf .lake/packages
|
||||
|
||||
$LAKE update
|
||||
# test that a second `lake update` is a no-op (with file paths)
|
||||
$LAKE update 2>&1 | diff - /dev/null
|
||||
$LAKE update --keep-toolchain 2>&1 | diff - /dev/null
|
||||
test -d .lake/packages/hello
|
||||
# test that Lake produces no warnings
|
||||
$LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null
|
||||
|
||||
@@ -75,8 +75,8 @@ pushd d
|
||||
git init
|
||||
git checkout -b master
|
||||
cat >>lakefile.lean <<EOF
|
||||
require b from git "../b" @ "master"
|
||||
require c from git "../c" @ "master"
|
||||
require b from git "../b" @ "master"
|
||||
EOF
|
||||
# make sure we pick up the version from b's manifest (a@1)
|
||||
$LAKE update -v 2>&1 | grep --color 'first commit in a'
|
||||
@@ -129,13 +129,20 @@ $LAKE update a -v
|
||||
git commit -am 'second commit in b'
|
||||
popd
|
||||
pushd a
|
||||
# a@4
|
||||
# a@4/main
|
||||
sed_i 's/third commit/fourth commit/' A.lean
|
||||
git commit -am 'fourth commit in a'
|
||||
popd
|
||||
pushd c
|
||||
# c@2
|
||||
echo '-- second commit in c' >>C.lean
|
||||
git commit -am 'second commit in c'
|
||||
popd
|
||||
pushd d
|
||||
# d: b@1 -> b@2 => a@1 -> a@3
|
||||
$LAKE update b -v
|
||||
# test that Lake does not update c
|
||||
grep --color 'second commit in c' .lake/packages/c/C.lean && exit 1 || true
|
||||
# test 119: pickup a@3 and not a@4
|
||||
grep --color 'third commit in a' .lake/packages/a/A.lean
|
||||
# test the removal of `c` from the manifest
|
||||
|
||||
1
src/lake/tests/env/test.sh
vendored
1
src/lake/tests/env/test.sh
vendored
@@ -13,6 +13,7 @@ $LAKE env | grep ".*=.*"
|
||||
# NOTE: `printenv` exits with code 1 if the variable is not set
|
||||
$LAKE env printenv LAKE
|
||||
$LAKE env printenv LAKE_HOME
|
||||
$LAKE env printenv LEAN
|
||||
$LAKE env printenv LEAN_GITHASH
|
||||
$LAKE env printenv LEAN_SYSROOT
|
||||
$LAKE env printenv LEAN_AR | grep --color ar
|
||||
|
||||
@@ -1,14 +1,7 @@
|
||||
{"version": "1.1.0",
|
||||
"packagesDir": ".lake/packages",
|
||||
"packages":
|
||||
[{"type": "path",
|
||||
"scope": "",
|
||||
"name": "foo",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inherited": false,
|
||||
"dir": "./foo",
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "bar",
|
||||
[{"url": "bar",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "foo",
|
||||
@@ -17,6 +10,13 @@
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": null,
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"type": "path",
|
||||
"scope": "",
|
||||
"name": "foo",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inherited": false,
|
||||
"dir": "./foo",
|
||||
"configFile": "lakefile.lean"}],
|
||||
"name": "«foo-bar»",
|
||||
"lakeDir": ".lake"}
|
||||
|
||||
@@ -11,13 +11,13 @@ export ELAN_TOOLCHAIN=test
|
||||
grep --color "error: bogus/bogus: could not materialize package: dependency has no explicit source and was not found on Reservoir"
|
||||
|
||||
./clean.sh
|
||||
$LAKE -f git.toml update
|
||||
$LAKE -f git.toml update --keep-toolchain
|
||||
# Test that barrels are not fetched for non-Reservoir dependencies
|
||||
$LAKE -v -f git.toml build @Cli:extraDep |
|
||||
grep --color "Cli:optBarrel" && exit 1 || true
|
||||
|
||||
./clean.sh
|
||||
$LAKE -f barrel.lean update
|
||||
$LAKE -f barrel.lean update --keep-toolchain
|
||||
# Test that a barrel is not fetched for an unbuilt dependency
|
||||
$LAKE -v -f barrel.lean build @test:extraDep |
|
||||
grep --color "Cli:optBarrel" && exit 1 || true
|
||||
@@ -53,11 +53,11 @@ LEAN_GITHASH=ec3042d94bd11a42430f9e14d39e26b1f880f99b \
|
||||
$LAKE -f barrel.lean build Cli --no-build
|
||||
|
||||
./clean.sh
|
||||
$LAKE -f require.lean update -v
|
||||
$LAKE -f require.lean update -v --keep-toolchain
|
||||
test -d .lake/packages/doc-gen4
|
||||
$LAKE -f require.lean resolve-deps # validate manifest
|
||||
|
||||
./clean.sh
|
||||
$LAKE -f require.toml update v
|
||||
$LAKE -f require.toml update -v --keep-toolchain
|
||||
test -d .lake/packages/doc-gen4
|
||||
$LAKE -f require.toml resolve-deps # validate manifest
|
||||
|
||||
@@ -4,6 +4,7 @@ open Lake DSL
|
||||
package bar where
|
||||
moreLeanArgs := #["-DmaxHeartbeats=888000"]
|
||||
|
||||
require baz from ".." / "baz"
|
||||
require leaf from ".." / "leaf" with NameMap.empty.insert `val "888000"
|
||||
|
||||
lean_lib X
|
||||
|
||||
0
src/lake/tests/order/baz/X.lean
Normal file
0
src/lake/tests/order/baz/X.lean
Normal file
7
src/lake/tests/order/baz/lakefile.lean
Normal file
7
src/lake/tests/order/baz/lakefile.lean
Normal file
@@ -0,0 +1,7 @@
|
||||
import Lake
|
||||
open Lake DSL
|
||||
|
||||
package baz where
|
||||
moreLeanArgs := #["-DmaxHeartbeats=999000"]
|
||||
|
||||
lean_lib X
|
||||
@@ -1,3 +1,3 @@
|
||||
rm -rf .lake foo/.lake bar/.lake leaf/.lake
|
||||
rm -f lake-manifest.json foo/lake-manifest.json bar/lake-manifest.json leaf/lake-manifest.json
|
||||
rm -rf .lake foo/.lake bar/.lake baz/.lake leaf/.lake
|
||||
rm -f lake-manifest.json foo/lake-manifest.json bar/lake-manifest.json baz/lake-manifest.json leaf/lake-manifest.json
|
||||
rm -f lake-manifest-1.json
|
||||
|
||||
@@ -10,13 +10,13 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
|
||||
# Later packages and libraries in the dependency tree shadow earlier ones.
|
||||
# https://github.com/leanprover/lean4/issues/2548
|
||||
|
||||
$LAKE update
|
||||
$LAKE update -v
|
||||
$LAKE build +A -v | grep --color 222000
|
||||
$LAKE build +A.B -v | grep --color 333000
|
||||
$LAKE build +A.B.C -v | grep --color 333000
|
||||
$LAKE build +X -v | grep --color 888000
|
||||
$LAKE build +Y -v | grep --color 666000
|
||||
$LAKE build +Z -v | grep --color 666000
|
||||
$LAKE build +X -v | grep --color 888000 # bar
|
||||
$LAKE build +Y -v | grep --color 666000 # order
|
||||
$LAKE build +Z -v | grep --color 666000 # leaf from order
|
||||
$LAKE exe Y | grep --color root
|
||||
|
||||
# Tests that `lake update` does not reorder packages in the manifest
|
||||
|
||||
1
src/lake/tests/toolchain/.gitignore
vendored
1
src/lake/tests/toolchain/.gitignore
vendored
@@ -1 +1,2 @@
|
||||
/foo
|
||||
lean-toolchain
|
||||
|
||||
@@ -1 +1,2 @@
|
||||
rm -rf foo
|
||||
rm -f lake-manifest.json lean-toolchain
|
||||
|
||||
6
src/lake/tests/toolchain/lakefile.lean
Normal file
6
src/lake/tests/toolchain/lakefile.lean
Normal file
@@ -0,0 +1,6 @@
|
||||
import Lake
|
||||
open System Lake DSL
|
||||
|
||||
package test
|
||||
|
||||
require foo from "foo"
|
||||
@@ -1,9 +1,9 @@
|
||||
#!/usr/bin/env bash
|
||||
set -euxo pipefail
|
||||
|
||||
# Tests that Lake rebuilds when toolchain changes
|
||||
# See https://github.com/leanprover/lake/issues/62
|
||||
# Requires Elan to download a toolchain
|
||||
LAKE=${LAKE:-../../../.lake/build/bin/lake}
|
||||
|
||||
# Tests which require Elan to download a toolchain
|
||||
|
||||
# skip if no elan found
|
||||
if ! command -v elan > /dev/null; then
|
||||
@@ -11,9 +11,20 @@ if ! command -v elan > /dev/null; then
|
||||
exit 0
|
||||
fi
|
||||
|
||||
# Test that Lake rebuilds when toolchain changes
|
||||
# See https://github.com/leanprover/lake/issues/62
|
||||
|
||||
TOOLCHAIN=leanprover/lean4:v4.0.0
|
||||
./clean.sh
|
||||
elan run --install leanprover/lean4:v4.0.0 lake new foo
|
||||
cd foo
|
||||
elan run leanprover/lean4:v4.0.0 lake build +Foo:olean -v | grep --color Foo.olean
|
||||
rm lean-toolchain
|
||||
${LAKE:-../../../.lake/build/bin/lake} build -v | grep --color Foo.olean
|
||||
elan run --install $TOOLCHAIN lake new foo
|
||||
pushd foo
|
||||
elan run $TOOLCHAIN lake build +Foo:olean -v | grep --color Foo.olean
|
||||
rm lean-toolchain # switch to Lake under test
|
||||
$LAKE build -v | grep --color Foo.olean
|
||||
popd
|
||||
|
||||
# Test Lake runs under the new toolchain after Lake updates it
|
||||
rm -f foo/lake-manifest.json
|
||||
echo $TOOLCHAIN > foo/lean-toolchain
|
||||
$LAKE update
|
||||
grep --color -F '"version": 5' lake-manifest.json
|
||||
|
||||
1
src/lake/tests/updateToolchain/.gitignore
vendored
Normal file
1
src/lake/tests/updateToolchain/.gitignore
vendored
Normal file
@@ -0,0 +1 @@
|
||||
lean-toolchain
|
||||
1
src/lake/tests/updateToolchain/a/lakefile.toml
Normal file
1
src/lake/tests/updateToolchain/a/lakefile.toml
Normal file
@@ -0,0 +1 @@
|
||||
name = "a"
|
||||
1
src/lake/tests/updateToolchain/b/lakefile.toml
Normal file
1
src/lake/tests/updateToolchain/b/lakefile.toml
Normal file
@@ -0,0 +1 @@
|
||||
name = "b"
|
||||
1
src/lake/tests/updateToolchain/clean.sh
Executable file
1
src/lake/tests/updateToolchain/clean.sh
Executable file
@@ -0,0 +1 @@
|
||||
rm -f lean-toolchain a/lean-toolchain b/lean-toolchain
|
||||
9
src/lake/tests/updateToolchain/lakefile.toml
Normal file
9
src/lake/tests/updateToolchain/lakefile.toml
Normal file
@@ -0,0 +1,9 @@
|
||||
name = "test"
|
||||
|
||||
[[require]]
|
||||
name = "a"
|
||||
path = "a"
|
||||
|
||||
[[require]]
|
||||
name = "b"
|
||||
path = "b"
|
||||
35
src/lake/tests/updateToolchain/test.lean
Normal file
35
src/lake/tests/updateToolchain/test.lean
Normal file
@@ -0,0 +1,35 @@
|
||||
import Lake.Util.Version
|
||||
|
||||
open Lake
|
||||
|
||||
def checkParse (tc : String) :=
|
||||
IO.println <| repr <| ToolchainVer.ofString tc
|
||||
|
||||
def checkLt (tc1 tc2 : String) :=
|
||||
IO.println <| decide <| ToolchainVer.ofString tc1 < ToolchainVer.ofString tc2
|
||||
|
||||
def test := do
|
||||
IO.println ""
|
||||
checkParse "leanprover/lean4:v4.13.0-rc1"
|
||||
checkParse "leanprover/lean4:nightly-2024-09-15"
|
||||
checkParse "leanprover/lean4-pr-releases:pr-release-101"
|
||||
checkParse "leanprover/lean:v4.1.0"
|
||||
checkParse "4.12.0"
|
||||
checkLt "4.6.0-rc1" "v4.6.0"
|
||||
checkLt "4.12.0" "leanprover/lean4:v4.13.0-rc1"
|
||||
checkLt "nightly-2024-09-08" "nightly-2024-10-09"
|
||||
checkLt "nightly-2024-09-08" "4.0.0"
|
||||
|
||||
/--
|
||||
info:
|
||||
Lake.ToolchainVer.release { toSemVerCore := { major := 4, minor := 13, patch := 0 }, specialDescr := "rc1" }
|
||||
Lake.ToolchainVer.nightly { year := 2024, month := 9, day := 15 }
|
||||
Lake.ToolchainVer.pr 101
|
||||
Lake.ToolchainVer.other "leanprover/lean:v4.1.0"
|
||||
Lake.ToolchainVer.release { toSemVerCore := { major := 4, minor := 12, patch := 0 }, specialDescr := "" }
|
||||
true
|
||||
true
|
||||
true
|
||||
false
|
||||
-/
|
||||
#guard_msgs in #eval test
|
||||
68
src/lake/tests/updateToolchain/test.sh
Executable file
68
src/lake/tests/updateToolchain/test.sh
Executable file
@@ -0,0 +1,68 @@
|
||||
#!/usr/bin/env bash
|
||||
set -euxo pipefail
|
||||
|
||||
LAKE=${LAKE:-../../.lake/build/bin/lake}
|
||||
|
||||
# Ensure Lake thinks there is a elan environment configured
|
||||
export ELAN_HOME=
|
||||
|
||||
# Tests the toolchain update functionality of `lake update`
|
||||
|
||||
RESTART_CODE=4
|
||||
|
||||
test_update(){
|
||||
ELAN=true $LAKE update 2>&1 | grep --color "updating toolchain to '$1'"
|
||||
cat lean-toolchain | diff - <(echo -n "$1")
|
||||
}
|
||||
|
||||
# Test toolchain version API
|
||||
$LAKE lean test.lean
|
||||
|
||||
# Test no toolchain information
|
||||
./clean.sh
|
||||
$LAKE update 2>&1 | grep --color "toolchain not updated; no toolchain information found"
|
||||
|
||||
# Test a single unknown candidate
|
||||
./clean.sh
|
||||
echo lean-a > a/lean-toolchain
|
||||
test_update lean-a
|
||||
|
||||
# Test a single known (PR) candidate
|
||||
./clean.sh
|
||||
echo pr-release-101 > a/lean-toolchain
|
||||
test_update leanprover/lean4-pr-releases:pr-release-101
|
||||
|
||||
# Test release comparison
|
||||
./clean.sh
|
||||
echo v4.4.0 > a/lean-toolchain
|
||||
echo v4.8.0 > b/lean-toolchain
|
||||
test_update leanprover/lean4:v4.8.0
|
||||
|
||||
# Test nightly comparison
|
||||
./clean.sh
|
||||
echo nightly-2024-10-01 > a/lean-toolchain
|
||||
echo nightly-2024-01-10 > b/lean-toolchain
|
||||
test_update leanprover/lean4:nightly-2024-10-01
|
||||
|
||||
# Test up-to-date root
|
||||
./clean.sh
|
||||
echo v4.4.0 > a/lean-toolchain
|
||||
echo v4.8.0 > b/lean-toolchain
|
||||
echo v4.10.0 > lean-toolchain
|
||||
$LAKE update 2>&1 | grep --color "toolchain not updated; already up-to-date"
|
||||
|
||||
# Test multiple candidates
|
||||
./clean.sh
|
||||
echo lean-a > a/lean-toolchain
|
||||
echo lean-b > b/lean-toolchain
|
||||
$LAKE update 2>&1 | grep --color "toolchain not updated; multiple toolchain candidates"
|
||||
|
||||
# Test manual restart
|
||||
./clean.sh
|
||||
echo lean-a > a/lean-toolchain
|
||||
ELAN= $LAKE update 2>&1 && exit 1 || [ $? = $RESTART_CODE ]
|
||||
|
||||
# Test elan restart
|
||||
./clean.sh
|
||||
echo lean-a > a/lean-toolchain
|
||||
ELAN=echo $LAKE update | grep --color "run --install lean-a lake update"
|
||||
@@ -241,36 +241,46 @@ void div2k(mpz & a, mpz const & b, unsigned k) {
|
||||
|
||||
uint8 mpz::mod8() const {
|
||||
mpz a;
|
||||
mpz_tdiv_r_2exp(a.m_val, m_val, 8);
|
||||
mpz_fdiv_r_2exp(a.m_val, m_val, 8);
|
||||
return static_cast<uint8>(a.get_unsigned_int());
|
||||
}
|
||||
|
||||
uint16 mpz::mod16() const {
|
||||
mpz a;
|
||||
mpz_tdiv_r_2exp(a.m_val, m_val, 16);
|
||||
mpz_fdiv_r_2exp(a.m_val, m_val, 16);
|
||||
return static_cast<uint16>(a.get_unsigned_int());
|
||||
}
|
||||
|
||||
uint32 mpz::mod32() const {
|
||||
mpz a;
|
||||
mpz_tdiv_r_2exp(a.m_val, m_val, 32);
|
||||
mpz_fdiv_r_2exp(a.m_val, m_val, 32);
|
||||
return static_cast<uint32>(a.get_unsigned_int());
|
||||
}
|
||||
|
||||
uint64 mpz::mod64() const {
|
||||
mpz r;
|
||||
mpz_tdiv_r_2exp(r.m_val, m_val, 64);
|
||||
mpz_fdiv_r_2exp(r.m_val, m_val, 64);
|
||||
mpz l;
|
||||
mpz_tdiv_r_2exp(l.m_val, r.m_val, 32);
|
||||
mpz_fdiv_r_2exp(l.m_val, r.m_val, 32);
|
||||
mpz h;
|
||||
mpz_tdiv_q_2exp(h.m_val, r.m_val, 32);
|
||||
mpz_fdiv_q_2exp(h.m_val, r.m_val, 32);
|
||||
return (static_cast<uint64>(h.get_unsigned_int()) << 32) + static_cast<uint64>(l.get_unsigned_int());
|
||||
}
|
||||
|
||||
int8 mpz::smod8() const {
|
||||
mpz a;
|
||||
mpz_tdiv_r_2exp(a.m_val, m_val, 8);
|
||||
return static_cast<int8>(a.get_int());
|
||||
return static_cast<int8>(mod8());
|
||||
}
|
||||
|
||||
int16 mpz::smod16() const {
|
||||
return static_cast<int16>(mod16());
|
||||
}
|
||||
|
||||
int32 mpz::smod32() const {
|
||||
return static_cast<int32>(mod32());
|
||||
}
|
||||
|
||||
int64 mpz::smod64() const {
|
||||
return static_cast<int64>(mod64());
|
||||
}
|
||||
|
||||
void power(mpz & a, mpz const & b, unsigned k) {
|
||||
@@ -952,30 +962,57 @@ void div2k(mpz & a, mpz const & b, unsigned k) {
|
||||
}
|
||||
|
||||
uint8 mpz::mod8() const {
|
||||
return static_cast<uint8>(m_digits[0] & 0xFFu);
|
||||
uint8 ret = static_cast<uint8>(m_digits[0] & 0xFFu);
|
||||
if (m_sign) {
|
||||
ret = -ret;
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
uint16 mpz::mod16() const {
|
||||
return static_cast<uint16>(m_digits[0] & 0xFFFFu);
|
||||
uint16 ret = static_cast<uint16>(m_digits[0] & 0xFFFFu);
|
||||
if (m_sign) {
|
||||
ret = -ret;
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
uint32 mpz::mod32() const {
|
||||
return static_cast<uint32>(m_digits[0]);
|
||||
uint32 ret = static_cast<uint32>(m_digits[0]);
|
||||
if (m_sign) {
|
||||
ret = -ret;
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
uint64 mpz::mod64() const {
|
||||
if (m_size == 1)
|
||||
return m_digits[0];
|
||||
else
|
||||
return m_digits[0] + (static_cast<uint64>(m_digits[1]) << 8*sizeof(mpn_digit));
|
||||
uint64 ret;
|
||||
if (m_size == 1) {
|
||||
ret = m_digits[0];
|
||||
}
|
||||
else {
|
||||
ret = m_digits[0] + (static_cast<uint64>(m_digits[1]) << 8*sizeof(mpn_digit));
|
||||
}
|
||||
if (m_sign) {
|
||||
ret = -ret;
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
int8 mpz::smod8() const {
|
||||
int8_t val = mod8();
|
||||
if (m_sign) {
|
||||
val = -val;
|
||||
}
|
||||
return val;
|
||||
return static_cast<int8>(mod8());
|
||||
}
|
||||
|
||||
int16 mpz::smod16() const {
|
||||
return static_cast<int16>(mod16());
|
||||
}
|
||||
|
||||
int32 mpz::smod32() const {
|
||||
return static_cast<int32>(mod32());
|
||||
}
|
||||
|
||||
int64 mpz::smod64() const {
|
||||
return static_cast<int64>(mod64());
|
||||
}
|
||||
|
||||
void power(mpz & a, mpz const & b, unsigned k) {
|
||||
|
||||
@@ -272,6 +272,9 @@ public:
|
||||
uint64 mod64() const;
|
||||
|
||||
int8 smod8() const;
|
||||
int16 smod16() const;
|
||||
int32 smod32() const;
|
||||
int64 smod64() const;
|
||||
|
||||
/**
|
||||
\brief Return the position of the most significant bit.
|
||||
|
||||
@@ -1566,6 +1566,18 @@ extern "C" LEAN_EXPORT int8 lean_int8_of_big_int(b_obj_arg a) {
|
||||
return mpz_value(a).smod8();
|
||||
}
|
||||
|
||||
extern "C" LEAN_EXPORT int16 lean_int16_of_big_int(b_obj_arg a) {
|
||||
return mpz_value(a).smod16();
|
||||
}
|
||||
|
||||
extern "C" LEAN_EXPORT int32 lean_int32_of_big_int(b_obj_arg a) {
|
||||
return mpz_value(a).smod32();
|
||||
}
|
||||
|
||||
extern "C" LEAN_EXPORT int64 lean_int64_of_big_int(b_obj_arg a) {
|
||||
return mpz_value(a).smod64();
|
||||
}
|
||||
|
||||
// =======================================
|
||||
// Float
|
||||
|
||||
|
||||
@@ -17,4 +17,48 @@ but is expected to have type
|
||||
#guard_msgs in
|
||||
theorem bug: True := by
|
||||
all_goals exact Nat.succ True
|
||||
trivial
|
||||
trace "Did not get here"
|
||||
|
||||
/-!
|
||||
Regression test: `all_goals` should admit goals rather than leaving metavariables.
|
||||
-/
|
||||
/--
|
||||
error: omega could not prove the goal:
|
||||
No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
|
||||
---
|
||||
error: omega could not prove the goal:
|
||||
No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
|
||||
---
|
||||
error: omega could not prove the goal:
|
||||
No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
|
||||
---
|
||||
error: omega could not prove the goal:
|
||||
No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
|
||||
-/
|
||||
#guard_msgs in
|
||||
theorem kernel_declaration_meta_variables (x y z : Option Int) : (x = y) ↔ (x = z) := by
|
||||
apply Iff.elim
|
||||
all_goals omega
|
||||
trace "Did not get here"
|
||||
|
||||
/-!
|
||||
Regression test: `all_goals` still respects recovery state.
|
||||
-/
|
||||
/-- warning: declaration uses 'sorry' -/
|
||||
#guard_msgs in
|
||||
example (x y z : Option Int) : (x = y) ↔ (x = z) := by
|
||||
apply Iff.elim
|
||||
first | all_goals omega | all_goals sorry
|
||||
|
||||
/-!
|
||||
Regression test: `all_goals` should not catch runtime exceptions.
|
||||
-/
|
||||
/--
|
||||
error: maximum recursion depth has been reached
|
||||
use `set_option maxRecDepth <num>` to increase limit
|
||||
use `set_option diagnostics true` to get diagnostic information
|
||||
-/
|
||||
#guard_msgs in
|
||||
example : False := by
|
||||
all_goals repeat try trivial
|
||||
trace "Did not get here"
|
||||
|
||||
@@ -1,3 +1,207 @@
|
||||
import Lean
|
||||
/-!
|
||||
# Tests of the `all_goals` tactic
|
||||
|
||||
This file aims to be a comprehensive test of the `all_goals` tactic combinator.
|
||||
-/
|
||||
|
||||
open Lean Elab Tactic
|
||||
|
||||
|
||||
/-!
|
||||
Tactics may assign other goals. There are three goals, but the tactic is run twice.
|
||||
-/
|
||||
/--
|
||||
info: case a
|
||||
⊢ 1 ≤ ?m
|
||||
|
||||
case a
|
||||
⊢ ?m ≤ 2
|
||||
|
||||
case m
|
||||
⊢ Nat
|
||||
---
|
||||
info: running tac
|
||||
running tac
|
||||
-/
|
||||
#guard_msgs in
|
||||
example : 1 ≤ 2 := by
|
||||
apply Nat.le_trans
|
||||
trace_state
|
||||
all_goals trace "running tac"; first | apply Nat.le_refl | simp
|
||||
|
||||
|
||||
/-!
|
||||
Each failing tactic gets its own error message when in recovery mode.
|
||||
There is no "unsolved goals" error.
|
||||
-/
|
||||
/--
|
||||
error: type mismatch
|
||||
Eq.refl 3
|
||||
has type
|
||||
3 = 3 : Prop
|
||||
but is expected to have type
|
||||
false = false : Prop
|
||||
---
|
||||
error: type mismatch
|
||||
Eq.refl 3
|
||||
has type
|
||||
3 = 3 : Prop
|
||||
but is expected to have type
|
||||
true = true : Prop
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (b : Bool) : b = b := by
|
||||
cases b
|
||||
all_goals exact Eq.refl 3
|
||||
trace "shouldn't get here"
|
||||
|
||||
|
||||
/-!
|
||||
Even if at least one suceeds, the entire tactic fails if any fails, stopping the tactic script.
|
||||
-/
|
||||
/--
|
||||
error: type mismatch
|
||||
Eq.refl true
|
||||
has type
|
||||
true = true : Prop
|
||||
but is expected to have type
|
||||
false = false : Prop
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (b : Bool) : b = b := by
|
||||
cases b
|
||||
all_goals exact Eq.refl true
|
||||
trace "shouldn't get here"
|
||||
|
||||
|
||||
/-!
|
||||
On failure, the metavar context is reverted. Here, `v` is temporarily assigned to `()` in the `true`
|
||||
case (see the first 'unsolved goals'), but then afterwards it is unassigned.
|
||||
-/
|
||||
/--
|
||||
error: unsolved goals
|
||||
v : Unit := ()
|
||||
this : () = v
|
||||
⊢ True
|
||||
---
|
||||
error: unsolved goals
|
||||
case refine_2.false
|
||||
v : Unit := ?_ false
|
||||
⊢ True
|
||||
|
||||
case refine_1
|
||||
b : Bool
|
||||
⊢ Unit
|
||||
---
|
||||
info: case refine_2.false
|
||||
v : Unit := ?_ false
|
||||
⊢ True
|
||||
|
||||
case refine_1
|
||||
b : Bool
|
||||
⊢ Unit
|
||||
-/
|
||||
#guard_msgs in
|
||||
set_option pp.mvars false in
|
||||
example (b : Bool) : True := by
|
||||
let v : Unit := ?_
|
||||
cases b
|
||||
case true =>
|
||||
all_goals (have : () = v := (by refine rfl); done)
|
||||
trace_state
|
||||
|
||||
|
||||
/-!
|
||||
On error, all goals are admitted. There are two `sorry`s in the prof term even though the tactic succeeds in one case.
|
||||
-/
|
||||
|
||||
/--
|
||||
error: type mismatch
|
||||
Eq.refl true
|
||||
has type
|
||||
true = true : Prop
|
||||
but is expected to have type
|
||||
false = false : Prop
|
||||
---
|
||||
info: Try this: Bool.casesOn (motive := fun t => b = t → b = b) b (fun h => Eq.symm h ▸ sorry) (fun h => Eq.symm h ▸ sorry)
|
||||
(Eq.refl b)
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (b : Bool) : b = b := by?
|
||||
cases b
|
||||
all_goals exact Eq.refl true
|
||||
|
||||
|
||||
/-!
|
||||
Each successive goal sees the metavariable assignments of the preceding ones, even if the preceding one failed.
|
||||
-/
|
||||
/--
|
||||
error: Case tag 'true' not found.
|
||||
|
||||
The only available case tag is 'refine_2.false'.
|
||||
---
|
||||
info: case refine_2.false
|
||||
v : Unit := ()
|
||||
this : () = v
|
||||
⊢ True
|
||||
case refine_2.true
|
||||
v : Unit := ()
|
||||
⊢ True
|
||||
---
|
||||
info: true
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (b : Bool) : True := by
|
||||
let v : Unit := ?_
|
||||
cases b
|
||||
all_goals
|
||||
try case' false => have : () = v := (by refine rfl)
|
||||
trace_state
|
||||
case true => trace "true"; trivial
|
||||
trace "should not get here"
|
||||
|
||||
|
||||
/-!
|
||||
When not in recovery mode, the first error becomes an exception.
|
||||
-/
|
||||
|
||||
elab "without_recover " tac:tactic : tactic => do
|
||||
withoutRecover <| evalTactic tac
|
||||
|
||||
/--
|
||||
error: type mismatch
|
||||
Eq.refl 3
|
||||
has type
|
||||
3 = 3 : Prop
|
||||
but is expected to have type
|
||||
false = false : Prop
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (b : Bool) : b = b := by
|
||||
cases b
|
||||
without_recover all_goals exact Eq.refl 3
|
||||
|
||||
|
||||
/-!
|
||||
When `all_goals` fails outside recovery mode, state is completely rolled back.
|
||||
This is the responsibility of `first`, but `all_goals` coordinates by being sure to throw an exception.
|
||||
-/
|
||||
|
||||
/--
|
||||
info: rfl
|
||||
rfl
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (b : Bool) : b = b := by
|
||||
cases b
|
||||
first | (all_goals exact Eq.refl false) | (all_goals trace "rfl"; rfl)
|
||||
|
||||
|
||||
/-!
|
||||
Various tests involving a `Weekday` type.
|
||||
-/
|
||||
|
||||
inductive Weekday where
|
||||
| sunday : Weekday
|
||||
| monday : Weekday
|
||||
|
||||
@@ -108,3 +108,11 @@ y = 0xffffffff#32
|
||||
#guard_msgs in
|
||||
example (x y : BitVec 32) (h1 : x.toNat = y.toNat) (h2 : x = zeros 32) : y = 0 := by
|
||||
bv_decide
|
||||
|
||||
/--
|
||||
error: The prover found a counterexample, consider the following assignment:
|
||||
x = 0x3#2
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (x : BitVec 2) : (bif x.ult 0#2 then 1#2 else 2#2) == 3#2 := by
|
||||
bv_decide
|
||||
|
||||
@@ -34,7 +34,8 @@
|
||||
#eval (10 : Int8) / -2 = -5
|
||||
#eval (10 : Int8) / 0 = 0
|
||||
#eval (10 : Int8) % 1 = 0
|
||||
#eval (10 : Int8) % 0 = 0
|
||||
#eval (10 : Int8) % 0 = 10
|
||||
#eval (-10 : Int8) % 0 = -10
|
||||
#eval (10 : Int8) % 3 = 1
|
||||
#eval (-10 : Int8) % 3 = -1
|
||||
#eval (-10 : Int8) % -3 = -1
|
||||
@@ -71,25 +72,278 @@
|
||||
#eval min (10 : Int8) 20 = 10
|
||||
#eval min (10 : Int8) (-1) = -1
|
||||
|
||||
def test : Option Int := Id.run do
|
||||
let doTest (base : Int) (i : Int) : Bool :=
|
||||
def test {α : Type} [BEq α] (w : Nat) (ofBitVec : BitVec w → α) (ofInt : Int → α)
|
||||
(ofNat : Nat → α) : Bool := Id.run do
|
||||
let doIntTest (base : Int) (i : Int) : Bool :=
|
||||
let t := base + i
|
||||
let a := ⟨⟨BitVec.ofInt 8 t⟩⟩
|
||||
let b := Int8.ofInt t
|
||||
let a := ofBitVec (BitVec.ofInt w t)
|
||||
let b := ofInt t
|
||||
a == b
|
||||
let doNatTest (base : Nat) (i : Nat) : Bool :=
|
||||
let t := base + i
|
||||
let a := ofBitVec (BitVec.ofInt w t)
|
||||
let b := ofNat t
|
||||
a == b
|
||||
|
||||
let range := 2^9
|
||||
|
||||
for i in [0:2*range] do
|
||||
let i := Int.ofNat i - range
|
||||
if !(doTest (2^256) i) then
|
||||
return i
|
||||
if !(doTest (-2^256) i) then
|
||||
return i
|
||||
return none
|
||||
|
||||
#eval test.isNone
|
||||
let range := 2^9
|
||||
|
||||
for c in [0:2*range] do
|
||||
let int := Int.ofNat c - range
|
||||
if !(doIntTest (2^256) int) then
|
||||
return false
|
||||
if !(doNatTest (2^256 - range) c) then
|
||||
return false
|
||||
if !(doIntTest (-2^256) int) then
|
||||
return false
|
||||
return true
|
||||
|
||||
#eval test 8 (⟨⟨·⟩⟩) Int8.ofInt Int8.ofNat
|
||||
|
||||
-- runtime representation
|
||||
set_option trace.compiler.ir.result true in
|
||||
def myId (x : Int8) : Int8 := x
|
||||
def myId8 (x : Int8) : Int8 := x
|
||||
|
||||
#check Int16
|
||||
#eval Int16.ofInt 20
|
||||
#eval Int16.ofInt (-20)
|
||||
#eval Int16.ofInt (-20) = -20
|
||||
#eval 2^15 - 10 = 32758 ∧ Int16.ofInt (-(2^15) - 10) = 32758
|
||||
#eval (10 : Int16) ≠ (11 : Int16)
|
||||
#eval (-10 : Int16) ≠ (10 : Int16)
|
||||
#eval Int16.ofNat 10 = 10
|
||||
#eval 2^15 + 10 = 32778 ∧ Int16.ofNat 32778 = 32778
|
||||
#eval Int16.ofNat 120 = 120
|
||||
#eval Int16.ofInt (-20) = -20
|
||||
#eval (Int16.ofInt (-2)).toInt = -2
|
||||
#eval (Int16.ofInt (-2)).toNat = 0
|
||||
#eval (Int16.ofInt (10)).toNat = 10
|
||||
#eval (Int16.ofInt (10)).toInt = 10
|
||||
#eval Int16.ofNat (2^64) == 0
|
||||
#eval Int16.ofInt (-2^64) == 0
|
||||
#eval Int16.neg 10 = -10
|
||||
#eval (20 : Int16) + 20 = 40
|
||||
#eval (2^15 - 1) = 32767 ∧ -2^15 = -32768 ∧ (32767 : Int16) + 1 = -32768
|
||||
#eval (-10 : Int16) + 10 = 0
|
||||
#eval (1 : Int16) - 2 = -1
|
||||
#eval (2^15 - 1) = 32767 ∧ -2^15 = -32768 ∧ (-32768 : Int16) - 1 = 32767
|
||||
#eval (1 : Int16) * 120 = 120
|
||||
#eval (2 : Int16) * 10 = 20
|
||||
#eval 65536 = 2^16 ∧ (2 : Int16) * 65536 = 0
|
||||
#eval (-1 : Int16) * (-1) = 1
|
||||
#eval (1 : Int16) * (-1) = -1
|
||||
#eval (2 : Int16) * (-10) = -20
|
||||
#eval (-5 : Int16) * (-5) = 25
|
||||
#eval (10 : Int16) / 2 = 5
|
||||
#eval (-10 : Int16) / 2 = -5
|
||||
#eval (-10 : Int16) / -2 = 5
|
||||
#eval (10 : Int16) / -2 = -5
|
||||
#eval (10 : Int16) / 0 = 0
|
||||
#eval (10 : Int16) % 1 = 0
|
||||
#eval (10 : Int16) % 0 = 10
|
||||
#eval (-10 : Int16) % 0 = -10
|
||||
#eval (10 : Int16) % 3 = 1
|
||||
#eval (-10 : Int16) % 3 = -1
|
||||
#eval (-10 : Int16) % -3 = -1
|
||||
#eval (10 : Int16) % -3 = 1
|
||||
#eval (10 : Int16) &&& 10 = 10
|
||||
#eval (-1 : Int16) &&& 1 = 1
|
||||
#eval (-1 : Int16) ^^^ 123 = ~~~123
|
||||
#eval (10 : Int16) ||| 10 = 10
|
||||
#eval (10 : Int16) ||| 0 = 10
|
||||
#eval (10 : Int16) ||| -1 = -1
|
||||
#eval (16 : Int16) >>> 1 = 8
|
||||
#eval (16 : Int16) >>> 16 = 16
|
||||
#eval (16 : Int16) >>> (16 + 1) = 8
|
||||
#eval (-16 : Int16) >>> 1 = -8
|
||||
#eval (16 : Int16) <<< 1 = 32
|
||||
#eval (16 : Int16) <<< (16 + 1) = 32
|
||||
#eval (-16 : Int16) <<< 1 = -32
|
||||
#eval (-16 : Int16) <<< (16 + 1) = -32
|
||||
#eval (-16 : Int16) >>> 1 <<< 1 = -16
|
||||
#eval (0 : Int16) < 1
|
||||
#eval (0 : Int16) < 120
|
||||
#eval (120 : Int16) > 0
|
||||
#eval -1 < (0 : Int16)
|
||||
#eval -120 < (0 : Int16)
|
||||
#eval ¬((0 : Int16) < (0 : Int16))
|
||||
#eval (0 : Int16) ≤ 1
|
||||
#eval (0 : Int16) ≤ 120
|
||||
#eval -1 ≤ (0 : Int16)
|
||||
#eval -120 ≤ (0 : Int16)
|
||||
#eval (0 : Int16) ≤ (0 : Int16)
|
||||
#eval (-10 : Int16) ≥ (-10 : Int16)
|
||||
#eval max (10 : Int16) 20 = 20
|
||||
#eval max (10 : Int16) (-1) = 10
|
||||
#eval min (10 : Int16) 20 = 10
|
||||
#eval min (10 : Int16) (-1) = -1
|
||||
|
||||
|
||||
#eval test 16 (⟨⟨·⟩⟩) Int16.ofInt Int16.ofNat
|
||||
|
||||
-- runtime representation
|
||||
set_option trace.compiler.ir.result true in
|
||||
def myId16 (x : Int16) : Int16 := x
|
||||
|
||||
|
||||
#check Int32
|
||||
#eval Int32.ofInt 20
|
||||
#eval Int32.ofInt (-20)
|
||||
#eval Int32.ofInt (-20) = -20
|
||||
#eval 2^31 - 10 = 2147483638 ∧ Int32.ofInt (-(2^31) - 10) = 2147483638
|
||||
#eval (10 : Int32) ≠ (11 : Int32)
|
||||
#eval (-10 : Int32) ≠ (10 : Int32)
|
||||
#eval Int32.ofNat 10 = 10
|
||||
#eval 2^31 + 10 = 2147483658 ∧ Int32.ofNat 2147483658 = 2147483658
|
||||
#eval Int32.ofNat 120 = 120
|
||||
#eval Int32.ofInt (-20) = -20
|
||||
#eval (Int32.ofInt (-2)).toInt = -2
|
||||
#eval (Int32.ofInt (-2)).toNat = 0
|
||||
#eval (Int32.ofInt (10)).toNat = 10
|
||||
#eval (Int32.ofInt (10)).toInt = 10
|
||||
#eval Int32.ofNat (2^64) == 0
|
||||
#eval Int32.ofInt (-2^64) == 0
|
||||
#eval Int32.neg 10 = -10
|
||||
#eval (20 : Int32) + 20 = 40
|
||||
#eval (2^31 - 1) = 2147483647 ∧ -2^31 = -2147483648 ∧ (2147483647 : Int32) + 1 = -2147483648
|
||||
#eval (-10 : Int32) + 10 = 0
|
||||
#eval (1 : Int32) - 2 = -1
|
||||
#eval (2^31 - 1) = 2147483647 ∧ -2^31 = -2147483648 ∧ (-2147483648 : Int32) - 1 = 2147483647
|
||||
#eval (1 : Int32) * 120 = 120
|
||||
#eval (2 : Int32) * 10 = 20
|
||||
#eval 4294967296 = 2^32 ∧ (2 : Int32) * 4294967296 = 0
|
||||
#eval (-1 : Int32) * (-1) = 1
|
||||
#eval (1 : Int32) * (-1) = -1
|
||||
#eval (2 : Int32) * (-10) = -20
|
||||
#eval (-5 : Int32) * (-5) = 25
|
||||
#eval (10 : Int32) / 2 = 5
|
||||
#eval (-10 : Int32) / 2 = -5
|
||||
#eval (-10 : Int32) / -2 = 5
|
||||
#eval (10 : Int32) / -2 = -5
|
||||
#eval (10 : Int32) / 0 = 0
|
||||
#eval (10 : Int32) % 1 = 0
|
||||
#eval (10 : Int32) % 0 = 10
|
||||
#eval (-10 : Int32) % 0 = -10
|
||||
#eval (10 : Int32) % 3 = 1
|
||||
#eval (-10 : Int32) % 3 = -1
|
||||
#eval (-10 : Int32) % -3 = -1
|
||||
#eval (10 : Int32) % -3 = 1
|
||||
#eval (10 : Int32) &&& 10 = 10
|
||||
#eval (-1 : Int32) &&& 1 = 1
|
||||
#eval (-1 : Int32) ^^^ 123 = ~~~123
|
||||
#eval (10 : Int32) ||| 10 = 10
|
||||
#eval (10 : Int32) ||| 0 = 10
|
||||
#eval (10 : Int32) ||| -1 = -1
|
||||
#eval (16 : Int32) >>> 1 = 8
|
||||
#eval (16 : Int32) >>> 32 = 16
|
||||
#eval (16 : Int32) >>> (32 + 1) = 8
|
||||
#eval (-16 : Int32) >>> 1 = -8
|
||||
#eval (16 : Int32) <<< 1 = 32
|
||||
#eval (16 : Int32) <<< (32 + 1) = 32
|
||||
#eval (-16 : Int32) <<< 1 = -32
|
||||
#eval (-16 : Int32) <<< (32 + 1) = -32
|
||||
#eval (-16 : Int32) >>> 1 <<< 1 = -16
|
||||
#eval (0 : Int32) < 1
|
||||
#eval (0 : Int32) < 120
|
||||
#eval (120 : Int32) > 0
|
||||
#eval -1 < (0 : Int32)
|
||||
#eval -120 < (0 : Int32)
|
||||
#eval ¬((0 : Int32) < (0 : Int32))
|
||||
#eval (0 : Int32) ≤ 1
|
||||
#eval (0 : Int32) ≤ 120
|
||||
#eval -1 ≤ (0 : Int32)
|
||||
#eval -120 ≤ (0 : Int32)
|
||||
#eval (0 : Int32) ≤ (0 : Int32)
|
||||
#eval (-10 : Int32) ≥ (-10 : Int32)
|
||||
#eval max (10 : Int32) 20 = 20
|
||||
#eval max (10 : Int32) (-1) = 10
|
||||
#eval min (10 : Int32) 20 = 10
|
||||
#eval min (10 : Int32) (-1) = -1
|
||||
|
||||
|
||||
#eval test 32 (⟨⟨·⟩⟩) Int32.ofInt Int32.ofNat
|
||||
|
||||
-- runtime representation
|
||||
set_option trace.compiler.ir.result true in
|
||||
def myId32 (x : Int32) : Int32 := x
|
||||
|
||||
#check Int64
|
||||
#eval Int64.ofInt 20
|
||||
#eval Int64.ofInt (-20)
|
||||
#eval Int64.ofInt (-20) = -20
|
||||
#eval 2^63 - 10 = 9223372036854775798 ∧ Int64.ofInt (-(2^63) - 10) = 9223372036854775798
|
||||
#eval (10 : Int64) ≠ (11 : Int64)
|
||||
#eval (-10 : Int64) ≠ (10 : Int64)
|
||||
#eval Int64.ofNat 10 = 10
|
||||
#eval 2^63 + 10 = 9223372036854775818 ∧ Int64.ofNat 9223372036854775818 = 9223372036854775818
|
||||
#eval Int64.ofNat 120 = 120
|
||||
#eval Int64.ofInt (-20) = -20
|
||||
#eval (Int64.ofInt (-2)).toInt = -2
|
||||
#eval (Int64.ofInt (-2)).toNat = 0
|
||||
#eval (Int64.ofInt (10)).toNat = 10
|
||||
#eval (Int64.ofInt (10)).toInt = 10
|
||||
#eval Int64.ofNat (2^64) == 0
|
||||
#eval Int64.ofInt (-2^64) == 0
|
||||
#eval Int64.neg 10 = -10
|
||||
#eval (20 : Int64) + 20 = 40
|
||||
#eval (2^63 - 1) = 9223372036854775807 ∧ -2^63 = -9223372036854775808 ∧ (9223372036854775807 : Int64) + 1 = -9223372036854775808
|
||||
#eval (-10 : Int64) + 10 = 0
|
||||
#eval (1 : Int64) - 2 = -1
|
||||
#eval (2^63 - 1) = 9223372036854775807 ∧ -2^63 = -9223372036854775808 ∧ (-9223372036854775808 : Int64) - 1 = 9223372036854775807
|
||||
#eval (1 : Int64) * 120 = 120
|
||||
#eval (2 : Int64) * 10 = 20
|
||||
#eval 18446744073709551616 = 2^64 ∧ (2 : Int64) * 18446744073709551616 = 0
|
||||
#eval (-1 : Int64) * (-1) = 1
|
||||
#eval (1 : Int64) * (-1) = -1
|
||||
#eval (2 : Int64) * (-10) = -20
|
||||
#eval (-5 : Int64) * (-5) = 25
|
||||
#eval (10 : Int64) / 2 = 5
|
||||
#eval (-10 : Int64) / 2 = -5
|
||||
#eval (-10 : Int64) / -2 = 5
|
||||
#eval (10 : Int64) / -2 = -5
|
||||
#eval (10 : Int64) / 0 = 0
|
||||
#eval (10 : Int64) % 1 = 0
|
||||
#eval (10 : Int64) % 0 = 10
|
||||
#eval (-10 : Int64) % 0 = -10
|
||||
#eval (10 : Int64) % 3 = 1
|
||||
#eval (-10 : Int64) % 3 = -1
|
||||
#eval (-10 : Int64) % -3 = -1
|
||||
#eval (10 : Int64) % -3 = 1
|
||||
#eval (10 : Int64) &&& 10 = 10
|
||||
#eval (-1 : Int64) &&& 1 = 1
|
||||
#eval (-1 : Int64) ^^^ 123 = ~~~123
|
||||
#eval (10 : Int64) ||| 10 = 10
|
||||
#eval (10 : Int64) ||| 0 = 10
|
||||
#eval (10 : Int64) ||| -1 = -1
|
||||
#eval (16 : Int64) >>> 1 = 8
|
||||
#eval (16 : Int64) >>> 64 = 16
|
||||
#eval (16 : Int64) >>> (64 + 1) = 8
|
||||
#eval (-16 : Int64) >>> 1 = -8
|
||||
#eval (16 : Int64) <<< 1 = 32
|
||||
#eval (16 : Int64) <<< (64 + 1) = 32
|
||||
#eval (-16 : Int64) <<< 1 = -32
|
||||
#eval (-16 : Int64) <<< (64 + 1) = -32
|
||||
#eval (-16 : Int64) >>> 1 <<< 1 = -16
|
||||
#eval (0 : Int64) < 1
|
||||
#eval (0 : Int64) < 120
|
||||
#eval (120 : Int64) > 0
|
||||
#eval -1 < (0 : Int64)
|
||||
#eval -120 < (0 : Int64)
|
||||
#eval ¬((0 : Int64) < (0 : Int64))
|
||||
#eval (0 : Int64) ≤ 1
|
||||
#eval (0 : Int64) ≤ 120
|
||||
#eval -1 ≤ (0 : Int64)
|
||||
#eval -120 ≤ (0 : Int64)
|
||||
#eval (0 : Int64) ≤ (0 : Int64)
|
||||
#eval (-10 : Int64) ≥ (-10 : Int64)
|
||||
#eval max (10 : Int64) 20 = 20
|
||||
#eval max (10 : Int64) (-1) = 10
|
||||
#eval min (10 : Int64) 20 = 10
|
||||
#eval min (10 : Int64) (-1) = -1
|
||||
|
||||
|
||||
#eval test 64 (⟨⟨·⟩⟩) Int64.ofInt Int64.ofNat
|
||||
|
||||
-- runtime representation
|
||||
set_option trace.compiler.ir.result true in
|
||||
def myId64 (x : Int64) : Int64 := x
|
||||
|
||||
@@ -71,13 +71,266 @@ true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
|
||||
[result]
|
||||
def myId (x_1 : u8) : u8 :=
|
||||
def myId8 (x_1 : u8) : u8 :=
|
||||
ret x_1
|
||||
def myId._boxed (x_1 : obj) : obj :=
|
||||
def myId8._boxed (x_1 : obj) : obj :=
|
||||
let x_2 : u8 := unbox x_1;
|
||||
dec x_1;
|
||||
let x_3 : u8 := myId x_2;
|
||||
let x_3 : u8 := myId8 x_2;
|
||||
let x_4 : obj := box x_3;
|
||||
ret x_4
|
||||
Int16 : Type
|
||||
20
|
||||
-20
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
|
||||
[result]
|
||||
def myId16 (x_1 : u16) : u16 :=
|
||||
ret x_1
|
||||
def myId16._boxed (x_1 : obj) : obj :=
|
||||
let x_2 : u16 := unbox x_1;
|
||||
dec x_1;
|
||||
let x_3 : u16 := myId16 x_2;
|
||||
let x_4 : obj := box x_3;
|
||||
ret x_4
|
||||
Int32 : Type
|
||||
20
|
||||
-20
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
|
||||
[result]
|
||||
def myId32 (x_1 : u32) : u32 :=
|
||||
ret x_1
|
||||
def myId32._boxed (x_1 : obj) : obj :=
|
||||
let x_2 : u32 := unbox x_1;
|
||||
dec x_1;
|
||||
let x_3 : u32 := myId32 x_2;
|
||||
let x_4 : obj := box x_3;
|
||||
ret x_4
|
||||
Int64 : Type
|
||||
20
|
||||
-20
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
true
|
||||
|
||||
[result]
|
||||
def myId64 (x_1 : u64) : u64 :=
|
||||
ret x_1
|
||||
def myId64._boxed (x_1 : obj) : obj :=
|
||||
let x_2 : u64 := unbox x_1;
|
||||
dec x_1;
|
||||
let x_3 : u64 := myId64 x_2;
|
||||
let x_4 : obj := box x_3;
|
||||
ret x_4
|
||||
|
||||
Reference in New Issue
Block a user