Skip to content

bootstrap HOTT at build time, close #90#99

Merged
mikeshulman merged 6 commits intomasterfrom
bootstrap
Aug 25, 2025
Merged

bootstrap HOTT at build time, close #90#99
mikeshulman merged 6 commits intomasterfrom
bootstrap

Conversation

@mikeshulman
Copy link
Collaborator

The new lib/hott compiles a temporary bootstrap executable, runs it at compile-time to typecheck the fibrancy code, and stores the typechecked version in the executable as a marshaled string so it can be loaded more quickly at run-time. My estimate in #90 was off for some reason, but this speeds up dune test by a factor of 2 for me right now, so it's still worth the trouble.

@mikeshulman mikeshulman merged commit 87d3b3a into master Aug 25, 2025
7 checks passed
@mikeshulman mikeshulman deleted the bootstrap branch August 25, 2025 21: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.

1 participant