Migrate Aeneas to the Lean module system - #1230
Conversation
…ey/aeneas into new-module-system
|
Note: The code produced by See Zulip discussion: #general > ✔ -gen-lib-entry creates all files at the root. |
| def U32.ofNatCore := @UScalar.ofNatCore .U32 | ||
| def U64.ofNatCore := @UScalar.ofNatCore .U64 | ||
| def U128.ofNatCore := @UScalar.ofNatCore .U128 | ||
| @[expose] def Usize.ofNatCore := @UScalar.ofNatCore .Usize |
There was a problem hiding this comment.
@[expose] section could be nice here
|
|
||
| def Post α := (α -> Prop) | ||
| def Pre := Prop | ||
| abbrev Post α := (α -> Prop) |
There was a problem hiding this comment.
| abbrev Post α := (α -> Prop) | |
| @[expose] def Post α := (α -> Prop) |
| def Post α := (α -> Prop) | ||
| def Pre := Prop | ||
| abbrev Post α := (α -> Prop) | ||
| abbrev Pre := Prop |
There was a problem hiding this comment.
| abbrev Pre := Prop | |
| @[expose] def Pre := Prop |
| abbrev Pre := Prop | ||
|
|
||
| def Wp α := Post α → Pre | ||
| abbrev Wp α := Post α → Pre |
There was a problem hiding this comment.
| abbrev Wp α := Post α → Pre | |
| @[expose] def Wp α := Post α → Pre |
| elab mods:declModifiers "impl_def " id:declId sig:optDeclSig val:declVal : command => do | ||
| let modifiers ← elabModifiers mods | ||
| let modifiers := | ||
| if modifiers.visibility matches .regular then { modifiers with visibility := .public } |
There was a problem hiding this comment.
This should ideally use the visibility from the surrounding scope rather than assuming it is .public
jeprinz
left a comment
jeprinz
left a comment
There was a problem hiding this comment.
I had some small nitpicks.
About the #assert issue, what is currently requiring assertions to compile the code is that computation of the tests depends on System.Platform.numBits, which is used in various places in aeneas and only computes when the code is compiled.
If there are any rust files that have both definitions and tests in them then maybe when use-lean-modules true it should just skip the tests?
2 participants
The PR is twofold:
This PR does the migration in the way that there is minimal change to the code and minimal effect to downstream users. As such, in general the full benefits of the module system aren't being used, instead many definitions are
@[expose]d in order to maintain the downstream proofs which took advantage of the visibility into all defs. This was done methodically in a way that something was only ever markedmetaif it was forced and something was only every markedexposeif that was required to keep downstream behaviour unchanged.That Aeneas uses the module system permits projects which depend on Aeneas to also benefit from the module system. Moreover, bit-by-bit parts of the Aeneas lean library can be updated to fully benefit from the module system.