8000 A few Makefile improvements by mtzguido · Pull Request #1034 · hacl-star/hacl-star · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

A few Makefile improvements #1034

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
Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open

A few Makefile improvements #1034

wants to merge 3 commits into from

Conversation

mtzguido
Copy link
Contributor

Proposed changes

Removing some of the substitutions needed for older F* versions. Now F* can

  • Take a checked file as input for extracting it (so no need to find the original fst 8000 )
  • Does not need --cache_checked_modules in order to read checked files, we always do it. We pass -c (an alias for the former) when we intend to write a checked file.
  • When extracting an OCaml file, we default to only extracting the modules passed in the cmdline, so some --extract_module are gone.

Types of changes

What types of changes does your code introduce to HACL*?
Put an x in the boxes that apply

  • Proof maintenance (non-breaking change which fixes a proof regression)
  • Bugfix (non-breaking change which fixes an issue)
  • New algorithm or feature (non-breaking change which adds functionality)
  • Improved performance (fix or feature that would improve performance of some algorithm on some platform)
  • Breaking change (fix or feature that would cause existing functionality to not work as expected)
  • Documentation Update (if none of the other choices apply)

Checklist

Put an x in the boxes that apply. You can also fill these out after creating the PR. If you're unsure about any of them, don't hesitate to ask. We're here to help! This is simply a reminder of what we are going to look for before merging your code.

  • I have read the CODE_OF_CONDUCT.md doc
  • I have read and agree to submit my changes under the LICENSE
  • I have added necessary documentation (if appropriate)
  • I have edited CHANGES.md (if appropriate)

@mtzguido mtzguido requested a review from a team as a code owner April 28, 2025 17:19
@msprotz
Copy link
Contributor
msprotz commented Apr 29, 2025
  • Is the empty prims.krml no longer generated?
  • Can we use the long option name instead of -c? -c is not super descriptive
    thanks!!

@mtzguido
Copy link
Contributor Author
  • Is the empty prims.krml no longer generated?

It's not, since FStarLang/FStar@3b67041 F* never puts it in ALL_KRML_FILES (and others). So I also added the last patch, thanks for noticing this!

The previous change was just removing the substitution prims -> Prims since Prims is now uppercase as every other module.

  • Can we use the long option name instead of -c? -c is not super descriptive

Done

mtzguido added 3 commits May 7, 2025 08:55
@mtzguido
Makefiles: simplify after F* changes
d36bc7e 
- No need to do fancy substitutions to extract, just point F* at a
  checked file.
- Use -o instead of --output_deps_to and --krmloutput
- Only pass --cache_checked_modules (-c) when trying to build a checked
  file, also use -o explicitly there.
@mtzguido
Makefile: remove substitution, prims is now Prims
a7f4677
@mtzguido
Makefiles: No need to filter-out prims.krml
676200e
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.
2 participants
@mtzguido @msprotz
0