Lef/everparse absolute fix by elefthei · Pull Request #4156 · FStarLang/FStar

elefthei · 2026-04-01T21:20:28Z

This removes conversion to absolute paths, and recursive directory traversal. It reverts to the previous fstar.include behavior.

The all_fstar_files_in_dir function was unconditionally recursing into all subdirectories when --dep was given a directory argument. This changes it to use Find.expand_include_d, which only recurses into subdirectories listed in fstar.include files. Without fstar.include, only F* files in the immediate directory are found. With fstar.include, only the listed subdirectories are traversed (matching the existing behavior of the include path mechanism). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

tahina-pro · 2026-04-01T22:13:28Z

Thanks a lot Lef!
I can confirm that, on EverParse fstar2 as of project-everest/everparse@68c594f, export ADMIT=1 && make -j cbor-snapshot && make -j cose-snapshot && make -j test works with this PR: .depend only contains relative paths, as expected.

tahina-pro · 2026-04-01T22:17:18Z

src/ml/FStarC_Filepath.ml

+  else
+    let path = normalize_file_path path in
+    let cwd  = normalize_file_path (Sys.getcwd ()) in
+    let split s = List.filter (fun x -> x <> "") (BatString.nsplit s ~by:"/") in


It may be better to use Filename.dir_sep to be portable with Windows
(cf. https://ocaml.org/manual/5.3/api/Filename.html)

tahina-pro · 2026-04-01T22:17:50Z

src/ml/FStarC_Filepath.ml

+    in
+    let (remaining_path, remaining_cwd) = skip_common path_parts cwd_parts in
+    let ups = List.map (fun _ -> "..") remaining_cwd in
+    String.concat "/" (ups @ remaining_path)


Same here: Filename.dir_sep

tahina-pro · 2026-04-01T22:19:25Z

src/ml/FStarC_Filepath.ml

+      | _ -> (pp, cp)
+    in
+    let (remaining_path, remaining_cwd) = skip_common path_parts cwd_parts in
+    let ups = List.map (fun _ -> "..") remaining_cwd in


OCaml has Filename.parent_dir_name, but since it is the same on all three of Windows, Linux and MacOS, we may not need to change this.

mtzguido · 2026-04-01T22:03:21Z

src/ml/FStarC_Filepath.ml

 (* Sys.is_directory raises Sys_error if the path does not exist *)
 let is_directory f = Sys.file_exists f && Sys.is_directory f

+let make_relative_to_cwd (path:string) : string =


This could probably be implemented directly via batteries. It looks OK for *nix, not sure about Windows due to backslashes?

mtzguido · 2026-04-01T22:22:17Z

src/parser/FStarC.Parser.Dep.fst

    let pr str = ignore <| FStarC.StringBuffer.add str sb in
-    let norm_path s = replace_chars (replace_chars s '\\' "/") ' ' "\\ " in
+    let norm_path s =
+      let s = Filepath.make_relative_to_cwd s in


So all paths will be relative now?

An explanation of why any absolute/relative distinction had to change would be useful. I feel like I'm still missing some context. I see this comment:

(** Expand any directories in the command line file list to their contained F* files. When a module has both .fst and .fsti, only include the .fsti to avoid "breaking abstraction" errors. *)

but I don't really understand it. Certainly it should not simply drop the fst since they are part of the dep analysis and should be verified+extracted etc.

Yes,

everparse uses (filter-out src/lowparse/lowparse.%) on .depend (there are reasons for that which I understand but are too long to explain here @tahina-pro can elaborate in person)

filter-out cannot take two wildcards (%src/lowparse/lowparse.%)

Those two reasons lead us to relative paths.

Just so that I understand, is this logic in everparse new? Or was it working before? F* used to emit a mixture of relative and absolute paths according to what was passed for --depend. E.g.

$ ls d1/* d2/* d1/X.fst d2/Y.fst $ fstar.exe --dep full --include d1 --include $(pwd)/d2 > a

Then ALL_FST_FILES has:

/home/guido/r/fstar/master/x/d2/Y.fst \ d1/X.fst

And it's the same for the targets:

d1/X.fst.checked: \ ... /home/guido/r/fstar/master/x/d2/Y.fst.checked: \ ...

Ok I understand that --include <relative or absolute> is the most general solution, I will do that.

I'm not sure it's that important, just trying to understand. If using relative paths does not break (many) things in other projects then I'm OK with it. But I'm not sure why this changed at all.

Just so that I understand, is this logic in everparse new? Or was it working before? F* used to emit a mixture of relative and absolute paths according to what was passed for --depend. E.g.

EverParse switched to a single Makefile for all dependencies in December 2024 at project-everest/everparse@19568d1 . It has been relying on relative --include paths for dependencies within EverParse, and absolute include paths for external dependencies (Karamel, Pulse, etc.) ever since.

tahina-pro · 2026-04-01T23:29:57Z

Alas, this change makes EverParse fstar2 break. For its main .depend, I am using relative --include paths. Now .depend contains an arbitrary mixture of absolute and relative paths: LowParse.Spec.Combinators.fsti has relative path, but LowParse.Spec.Combinators.fst has absolute path.
Then, ADMIT=1 make lowparse completes without producing LowParse.Spec.Combinators.fst.checked, which makes ADMIT=1 make asn1-test fail.

tahina-pro

See #4156 (comment)

elefthei · 2026-04-02T01:44:52Z

I don't get it, this is the previous behavior according to @mtzguido

mtzguido · 2026-04-02T14:38:50Z

There is still a diff compared to F* master. This is a fraction of the diff I get for ALL_CHECKED_FILES in .depend in everparse.

diff --git a/a b/b
index 9d92599..7baf62e 100644
--- a/a
+++ b/b
@@ -1,22 +1,25 @@
 ALL_CHECKED_FILES= \
        src/3d/prelude/EverParse3d.Prelude.fsti.checked \
-       src/cddl/pulse/CDDL.Pulse.Serialize.Gen.MapGroup.ZeroOrMore.Aux2.Lemma11.fst.checked \
-       src/cbor/spec/raw/CBOR.Spec.Raw.fst.checked \
+       /home/guido/r/everparse/main/src/cddl/pulse/CDDL.Pulse.Serialize.Gen.MapGroup.Choice.fst.checked \
+       /home/guido/r/everparse/main/src/cddl/pulse/CDDL.Pulse.Serialize.Gen.MapGroup.ZeroOrMore.Aux2.LoopBody.fst.checked \
        src/cddl/pulse/CDDL.Pulse.AST.Ancillaries.fst.checked \
        src/cbor/pulse/raw/CBOR.Pulse.API.Det.Rust.fst.checked \
-       src/cddl/spec/CDDL.Spec.MapGroup.fst.checked \
        src/cbor/pulse/raw/CBOR.Pulse.Raw.Format.Serialized.fsti.checked \
        src/cddl/pulse/CDDL.Pulse.Serialize.Gen.MapGroup.ZeroOrMore.Aux2.Proof0.fsti.checked \
+       /home/guido/r/everparse/main/src/3d/prelude/EverParse3d.Prelude.fst.checked \
        src/lowparse/LowParse.Low.DepLen.fst.checked \
-       src/3d/prelude/EverParse3d.Kinds.fst.checked \
        src/cbor/pulse/CBOR.Pulse.API.Det.C.Copy.fsti.checked \
        src/lowparse/LowParse.Tot.List.fst.checked \
+       /home/guido/r/everparse/main/src/lowparse/LowParse.SLow.Int.fst.checked \
+       /home/guido/r/everparse/main/src/cddl/pulse/CDDL.Pulse.Serialize.Gen.MapGroup.ZeroOrMore.Aux2.Lemma8.fst.checked \
        src/cddl/pulse/CDDL.Pulse.Parse.ArrayGroup.fst.checked \
        src/lowparse/LowParse.Low.Tac.Sum.fst.checked \
        src/cbor/spec/CBOR.Spec.Constants.fst.checked \
-       src/lowparse/LowParse.Low.BoundedInt.fst.checked \
        src/lowparse/LowParse.Tot.Base.fst.checked \
+       /home/guido/r/everparse/main/src/cddl/pulse/CDDL.Pulse.Serialize.Gen.MapGroup.ZeroOrMore.Aux2.Invariant.fst.checked \
        src/lowparse/LowParse.Spec.Bytes.fst.checked \
+       /home/guido/r/everparse/main/src/3d/prelude/EverParse3d.ProbeActions.fst.checked \
+       /home/guido/r/everparse/main/src/cddl/pulse/CDDL.Pulse.Serialize.Gen.MapGroup.ZeroOrMore.Aux2.Lemma3.fst.checked \
        src/cddl/pulse/CDDL.Pulse.AST.Env.fst.checked \
        src/cddl/pulse/CDDL.Pulse.Serialize.Gen.MapGroup.Map.fsti.checked \
        src/cbor/pulse/raw/CBOR.Pulse.Raw.Nondet.Compare.fst.checked \
@@ -24,15 +27,16 @@ ALL_CHECKED_FILES= \
        src/cbor/spec/raw/CBOR.Spec.Raw.Format.MapPair.fsti.checked \
        src/cddl/pulse/CDDL.Pulse.Serialize.Gen.MapGroup.ZeroOrMore.Aux2.Lemma8.fsti.checked \
        src/cddl/pulse/CDDL.Pulse.Serialize.Gen.MapGroup.ZeroOrMore.Aux2.Lemma13.fsti.checked \
+       /home/guido/r/everparse/main/src/cddl/pulse/CDDL.Pulse.Serialize.Gen.MapGroup.ZeroOrMore.Aux2.Lemma6.fst.checked \
        src/lowparse/LowParse.Spec.Combinators.fsti.checked \
        src/lowparse/LowParse.Spec.AllIntegers.fst.checked \
        src/cbor/pulse/raw/CBOR.Pulse.Raw.Read.fst.checked \
+       /home/guido/r/everparse/main/src/3d/prelude/EverParse3d.Kinds.fst.checked \
        src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.EverParse.Nondet.Basic.fst.checked \
        src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.EverParse.Format.fsti.checked \
        src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.EverParse.Serialized.Base.fsti.checked \
        src/lowparse/LowParse.SLow.BitSum.fst.checked \
        src/cddl/pulse/CDDL.Pulse.AST.Types.fst.checked \
-       src/lowparse/LowParse.SLow.Int.fst.checked \

mtzguido · 2026-04-02T14:49:45Z

I think the problem is this line added by the Dune PR:

   let all_cmd_line_files = expand_directories all_cmd_line_files in

In Everparse, the depend call is passed a long list of 412 files including fst's and fsti's. There are no directories to expand (as this is a new feature). However, the function unconditionally removes fsts for which an fsti was "found" (74 in total). Even with the patch here to respect fstar.include, the fsts get dropped, and rediscovered via the include path, and get an absolute path.

Removing this line makes things work as before. I now understand Tahina's PR a bit better, and see how that fixes it. But I still don't understand why this filtering is here at all. Can anyone explain, or can we remove it?

elefthei · 2026-04-02T17:24:32Z

thanks for removing the filter!

mtzguido · 2026-04-02T17:24:59Z

I removed the filtering. Everparse's .depend now looks as before AFAICT (there are many removals due to some modules of F*'s library being gone since my last build). examples/hello seems to work still.

elefthei requested review from mtzguido and tahina-pro April 1, 2026 21:20

tahina-pro reviewed Apr 1, 2026

View reviewed changes

mtzguido reviewed Apr 1, 2026

View reviewed changes

elefthei force-pushed the lef/everparse-absolute-fix branch from 5061426 to 04c562e Compare April 1, 2026 23:04

tahina-pro requested changes Apr 1, 2026

View reviewed changes

mtzguido added 2 commits April 2, 2026 10:18

Parser.Dep: remove strange fst filtering

87ec611

Merge branch 'fstar2' of gh:FStarLang/FStar

41712d4

mtzguido approved these changes Apr 2, 2026

View reviewed changes

mtzguido mentioned this pull request Apr 2, 2026

Parser.Dep: fix expand_directories filtering explicit cmd-line files #4144

Closed

Conversation

elefthei commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tahina-pro commented Apr 1, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

elefthei Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tahina-pro Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tahina-pro commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tahina-pro left a comment

Choose a reason for hiding this comment

Uh oh!

elefthei commented Apr 2, 2026

Uh oh!

mtzguido commented Apr 2, 2026

Uh oh!

mtzguido commented Apr 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

elefthei commented Apr 2, 2026

Uh oh!

mtzguido commented Apr 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

elefthei commented Apr 1, 2026 •

edited

Loading

elefthei Apr 1, 2026 •

edited

Loading

tahina-pro Apr 1, 2026 •

edited

Loading

tahina-pro commented Apr 1, 2026 •

edited

Loading

mtzguido commented Apr 2, 2026 •

edited

Loading