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

refactor(engine/fstar-ast): get rid of zarith and GMP #734

Merged
merged 2 commits into from
Jun 26, 2024

Conversation

W95Psp
Copy link
Collaborator

@W95Psp W95Psp commented Jun 24, 2024

This helps for #696: this PR gets rid of the dependency to the native lib gmp.
That's virtually the only native lib used by the engine, so we can (almost) consider binaries to be static from now on, that will do the trick at least for MacOS

Technically, this PR:

  • remove a bunch of useless code from the F* parser & AST
  • kills the dependency to zarith, replacing zarith's integers with... strings. That is fine since those integers are mainly used to represent constants in the AST

Copy link
Member

@franziskuskiefer franziskuskiefer left a comment

Choose a reason for hiding this comment

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

Nice! Deleting code!

@W95Psp W95Psp force-pushed the engine-kill-gmp-dependency branch from 3f4d2c9 to 6013d42 Compare June 26, 2024 08:53
@W95Psp W95Psp enabled auto-merge June 26, 2024 08:53
@W95Psp W95Psp added this pull request to the merge queue Jun 26, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Jun 26, 2024
@W95Psp W95Psp force-pushed the engine-kill-gmp-dependency branch from a4f5568 to ca15743 Compare June 26, 2024 14:18
@W95Psp W95Psp enabled auto-merge June 26, 2024 14:18
@W95Psp W95Psp added this pull request to the merge queue Jun 26, 2024
Merged via the queue into main with commit 22b75d5 Jun 26, 2024
13 checks passed
@W95Psp W95Psp deleted the engine-kill-gmp-dependency branch June 26, 2024 15:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
No open projects
Status: Done
Development

Successfully merging this pull request may close these issues.

2 participants