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.

Sign up for GitHub

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

Jump to bottom

Using typeclasses in src/ #2969

Merged
merged 10 commits into from
Nov 27, 2023
Merged

Using typeclasses in src/ #2969

merged 10 commits into from
Nov 27, 2023

Conversation

mtzguido
Copy link
Member

This is still a draft, but here's what it would take.

  • First move the rest of the tactics/reflection modules that point to the compiler into the FStar.Stubs namespace, this allows to mention the TAC effect within the compiler without being circular.

Then, since now a lot more of ulib is in the dep graph of the compiler:

  • Sort out the use of MLish, and never use it on ulib/.
  • Extract the compiler with --codegen Plugin, otherwise bootstrapping can race and sometimes we end up with registered plugins and sometimes not. This is a symptom of some modules being extracted twice since src/ and ulib/ have separate --dep invocations and are different make jobs.

@mtzguido mtzguido mentioned this pull request Aug 24, 2023
Merged
@mtzguido mtzguido marked this pull request as ready for review November 27, 2023 09:01
@mtzguido
Copy link
Member Author

Updated this PR and tidied a bit, I think it can be merged. Maybe @tahina-pro would be interested in the makefile changes.

@mtzguido
Makefile.boot: --MLish is never used for ulib/, yes for everything else
a615721
@mtzguido
Makefile.boot: compiler extracts with --codegen Plugin
23440a5
@mtzguido
Compiler: 'Stubbing' everything
cd67c6e 
To prevent circularities when using typeclasses within the compiler
(since we need to refer to tactic modules potentially from anywhere)
we stub all of the exposed interfaces in ulib, so the compiler does
not 'realize' they are the same modules. Extraction then takes care of
removing the 'Stubs' namespace component, essentially closing the loop.
@mtzguido
Introduce src/class and FStar.Compiler.Show
b5c505f
@mtzguido
Tactics: small example using show
da7a20a
@mtzguido
Introduce FStar.Class.PP
0483c42
@mtzguido
snap
117a847
@mtzguido mtzguido mentioned this pull request Nov 27, 2023
Merged
@mtzguido
Update expected output
97f7dfc 
Now mentions Stubs
@mtzguido mtzguido merged commit 39cb9fd into FStarLang:master Nov 27, 2023
2 checks passed
@mtzguido mtzguido deleted the guido_tc_in_src branch November 27, 2023 21:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@mtzguido