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

Moving compiler sources into the FStarC namespace #3557

Merged
merged 6 commits into from
Oct 11, 2024

Conversation

mtzguido
Copy link
Member

The library and the compiler have been sharing and punning modules for a long time, which complicates making sense of the build and changing one of them without affecting the other. This PR puts all of the compiler into the FStarC namespace, completely separate from FStar, the library.

This is in preparation for a staged build, but already an improvement and "noisy" so I'd like to merge this first to avoid bitrot. I in fact mostly produced this using the staged build, or it would have been a nightmare.

Some subprojects need patches: both Steel and Pulse define their own extraction passes which interact with compiler internals, so they need renaming. Since they compile with --MLish they also need the --MLish_effect FStarC.Compiler.Util option (#3548). Everparse/3D reuses FStar.Getopt from the compiler, so it needs an update too.

Projects using normal plugins should not need a patch (HACL* doesn't).

The namespaces could definitely be improved (e.g. FStarC.Compiler.Range is redundant). That will be a separate PR possibly after the staged build. I think that one should not break anything of this sort.

Companion branches:
https://github.com/mtzguido/pulse/tree/fstarc (there is a script in here that is handy for the renaming)
https://github.com/mtzguido/steel/tree/fstarc
https://github.com/mtzguido/everparse/tree/fstarc

Note: the support ML files for the library and the compiler are still all in ocaml/fstar-lib. The staged build will separate them.

cc @nikswamy @aseemr, does this look OK? It's hard to review, but wondering if you buy the plan.

@mtzguido
Copy link
Member Author

I have a local everest green with the following hashes

Executing in merkle-tree
e905cd82f7e6fd734062e9d0bf8a9d4b02a7b8e8 (HEAD, origin/main, origin/HEAD, main) hints

Executing in mitls-fstar
e9805d0173eb6f8addcca6ea8ad4e7c8f2046689 (HEAD, origin/master, origin/HEAD, master) also disable test

Executing in hacl-star
dfc6900f905953ba584265a7a1690f1681a0e468 (HEAD, origin/main, origin/HEAD, main) Merge pull request #990 from mtzguido/valedepend

Executing in karamel
84f64da8e4eb8b0d6d9c3fe75fcd116ee28e67d8 (HEAD, origin/master, origin/HEAD, master) Merge pull request #490 from mtzguido/move_fstar_io

Executing in everquic-crypto
6d73306fea04f22768fb876db5c092f4ac4fe60d (HEAD, origin/master, origin/HEAD, master) update hints while at it

Executing in MLCrypto
190250bbb8f16e7c3f6a8d443b13600ada4fbe79 (HEAD, origin/master, origin/HEAD, master) No longer build CoreCrypto

Executing in pulse
13d478ca285f64a960c6590217bcab20491afa8d (HEAD, mine/fstarc) snap, as usual

Executing in steel
e13b3d2f6c504bf872d84d792d3d84ae8eb543ef (HEAD, mine/fstarc) snap

Executing in everparse
6e15b95216e11ee4f4c5b17eba0dc73de9baef10 (HEAD, mine/fstarc) Moving FStar.Getopt -> FStarC.Getopt

@nikswamy
Copy link
Collaborator

I buy the plan!

@mtzguido
Copy link
Member Author

Merging and opening PRs in the subprojects!

@mtzguido mtzguido merged commit 0dcfea3 into FStarLang:master Oct 11, 2024
2 checks passed
@mtzguido mtzguido deleted the fstarc branch October 11, 2024 08:01
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.

2 participants