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

Introduce --read_checked_file option #3381

Merged
merged 3 commits into from
Aug 17, 2024

Conversation

mtzguido
Copy link
Member

This PR introduces an option to make F* read a checked file and print it out (the tc_module in it, actually). It does not involve any include path, or finding the corresponding file, or parsing: it just reads whatever file the user passes in and prints it to standard output.

$ ./bin/fstar.exe --read_checked_file ulib/.cache/prims.fst.checked
module Prims
Declarations: [
assume new
val attribute:Type0
assume
val cps:Prims.attribute
assume
val hasEq (_: Type) : Prims.GTot Type0
let eqtype = a: Type0{Prims.hasEq a}
assume new
val bool:Prims.eqtype
type empty =
type trivial = | T : Prims.trivial

assume new
val unit:Prims.eqtype
let squash p = x: Prims.unit{p}
let auto_squash p = Prims.squash p
private
let logical = Type0
[...]

It would be nicer if we improve the format of modul_to_string, since it currently displays everything twice. See this comment:

(*
 * AR: 07/19: exports is redundant, keeping it here until vale is fixed to not parse it
 *)
let modul_to_string (m:modul) =
  U.format3 "module %s\nDeclarations: [\n%s\n]\nExports: [\n%s\n]\n" (sli m.name)
                                                                     (List.map sigelt_to_string m.declarations |> String.concat "\n")
                                                                     (List.map sigelt_to_string m.declarations |> String.concat "\n")

@mtzguido
Copy link
Member Author

I'm merging this since it could be useful. We can also consider printing other pieces of the checked file (deps, hashes, etc).

@mtzguido mtzguido merged commit e02d25f into FStarLang:master Aug 17, 2024
2 checks passed
@mtzguido mtzguido deleted the read_checked_file branch August 17, 2024 21:48
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