Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

docs: init first sketch #294

Open
wants to merge 8 commits into
base: main
Choose a base branch
from

Conversation

RaitoBezarius
Copy link
Contributor

@RaitoBezarius RaitoBezarius commented Aug 10, 2024

This is a first sketch of user documentation for Aeneas to prove things with Lean.

This adds a factorial example with Alectryon and scaffolding from the Lean original project.

Makefile Outdated Show resolved Hide resolved
Makefile Outdated Show resolved Hide resolved
scripts/update-charon-pin.sh Outdated Show resolved Hide resolved
@RaitoBezarius RaitoBezarius force-pushed the proving-with-lean branch 3 times, most recently from 2931670 to be14c6a Compare August 26, 2024 14:43
@RaitoBezarius
Copy link
Contributor Author

PTAL @sonmarcho I dropped the irrelevant parts.

@RaitoBezarius
Copy link
Contributor Author

RaitoBezarius commented Aug 27, 2024

@sonmarcho In principle, I updated to 4.11.0-rc2 and confirmed it built on my system, let's see how it goes.
I included an micro-guide of docs on how to update in 3a1d6bc but I will add one in an upcoming PR.

Ryan Lahfa added 6 commits August 27, 2024 17:03
This is a first sketch of user documentation for Aeneas to prove things
with Lean.

Signed-off-by: Ryan Lahfa <[email protected]>
Well, this is required… Following Loogle's steps, we add fake files for
ProofWidgets4 and we can produce an .olean from Aeneas' base library
without Lake involvement!

Free parallelization and caching :).

TODOs are to improve the hash handling when lake-manifest.json bumps,
but this requires extending Lake to produce the NAR hash serializations.

Signed-off-by: Ryan Lahfa <[email protected]>
I extracted a Factorial example in Rust to Lean.

Signed-off-by: Ryan Lahfa <[email protected]>
As upstream is moving to a non-user-facing Nix library,
we are vendoring some of the useful code such as `buildLeanPackage`.

Signed-off-by: Ryan Lahfa <[email protected]>
Adds the TODO list for infrastructure.

Signed-off-by: Ryan Lahfa <[email protected]>
Micro-guide for update:

- Update the Lean flake.
- Update all the sha256 hashes of every dependency if you have a
compilation error, e.g. batteries changed, etc.

The day where `inputs.lean.packages.${system}.deprecated` disappear, we
will need to consider an alternative for the nixpkgs from lean, etc.

Signed-off-by: Ryan Lahfa <[email protected]>
@RaitoBezarius RaitoBezarius marked this pull request as ready for review August 27, 2024 15:03
@RaitoBezarius
Copy link
Contributor Author

RaitoBezarius commented Aug 27, 2024

@pnmadelaine We will need a cache for the userdocs part because it will compile Mathlib4 in Nix and if we do it at each rerun, this will be very expensive. I forgot we are using self hosted runners.

@sonmarcho
Copy link
Member

This is great, thanks!! I will review and merge asap.


The Nix setup reads the `lakefile-manifest.json`, but this lockfile is insufficient to lock purely the dependencies (NAR SHA256 serialization are missing).

To overcome this, they are specified manually in `flake.nix`, but each time the Aeneas standard library updates their dependencies, the `flake.nix` needs to have all its hash rewritten.
Copy link
Member

@sonmarcho sonmarcho Aug 28, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't fully understand what we are supposed to do when updating the dependencies.
With regards to that, I guess adding some comments in the flake.nix would be useful?...

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I expanded much more the documentation, let me know how you feel about it now

docs/user/README.md Outdated Show resolved Hide resolved
@@ -0,0 +1,190 @@
var Alectryon;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This file also comes from Alectryon right? There are no copyrights (that's surprising)?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

https://github.com/cpitclaudel/alectryon/blob/2a544230290be6dd84f0ce736e86f8a071d70739/alectryon/assets/alectryon.js#L4

Yep, but this is how it is upstream, I am fine with adding the compliance copyright, what do you prefer?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(may be worth investigating https://reuse.software/ if we want to maximize the licensing compliance situation)

Copy link
Member

@sonmarcho sonmarcho left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is great, thanks!
I put a few questions, and am also wondering: you mention that the files to process should be put in lean/basics/. But what about the other folders? For instance lean/bst?

@RaitoBezarius
Copy link
Contributor Author

This is great, thanks! I put a few questions, and am also wondering: you mention that the files to process should be put in lean/basics/. But what about the other folders? For instance lean/bst?

I updated the docs, but there's a section on this.
Other directories that are not listed as roots of the literate Lean meta package does not get their Lean files processed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants