Staged build, new CI, new packaging

[mtzguido]

Still a draft, posting for visibiblity

A mostly green local + friends CI here: https://github.com/mtzguido/FStar/actions/runs/12359614442/attempts/1

Missing:

• Nix build
• Test this on cygwin, it will likely fail in all sorts of ways as F* is currently broken wrt paths.

[gebner]

The F# files are all renamed to XX_*. Does this PR drop support for F# extraction?

[gebner]

This should use the new get_fstar_z3.sh script.

[gebner]

Should we append this step to build to reduce CI usage?

[mtzguido]

I was wondering how best to split all this.. doing that does save on total usage, but splitting it away reduces the time until the test jobs can start. (Testing could also be done in this same job, which would maximize parallelism with stage3, but I liked the idea of a starting from a clean slate, and allows subprojects to be checked even if some test fails.) Another bonus is that if the stage3 diff fails for some reason, we still go ahead with normal tests.

Maybe we can just record the state of the repo in an artifact (in fact it's done already, for Pulse) and start the stage3 check from there... wdyt?

[gebner]

Maybe we can just record the state of the repo in an artifact (in fact it's done already, for Pulse) and start the stage3 check from there... wdyt?

That's probably the best idea.

[gebner]

Should we really build the whole world on every push?

[mtzguido]

No, that's just temporary while we work on this. I think the consensus is to run internal F* tests to allow merges to dev, and a world check for master.

[gebner]

Let's not forget to turn it off before merging then!

[gebner]

I still think it's a bad idea to make the default F* binary point to whatever make target succeeded last, and this will likely confuse the hell out of me.

It's great that you changed the ulib vscode config to point to stage1 directly (and src to stage0). That addresses most of my practical concerns with debugging failing builds.

[mtzguido]

I tend to agree, but I think we'll want a way to be able to run the tests on the stage 1 compiler. Currently that's as easy as make 1 && make test. Note that the out link is only created when you call make 1 or make 2. Most users will not use these rules and just get the stage 2 compiler, i.e. the actual final product.

I'd also be happy having a differently named rule for setting the link to the stage 1, fake-1 or whatever.

[gebner]

I think the most natural way to run tests is make test; and I'd expect that it would be roughly similar to CI, i.e., it should build F* and run the tests on stage 2.

I also just realized that make test by itself would fail (or use an out-of-date fstar.exe) since it doesn't depend on any build target. That's really unexpected.

Another options is to have test-1 and test-2 targets, and maybe test: test-2 for convenience. (Then the tests could also use different cache directories for each stage if we want to support that.)

Most users will not use these rules

What you're saying is that if you only ever call make, then this defaults to make 2 and you'll only ever get a symlink to stage 2, right?

Is there a target to build stage N without messing with the symlinks?

[mtzguido]

I think the most natural way to run tests is make test; and I'd expect that it would be roughly similar to CI, i.e., it should build F* and run the tests on stage 2.

I also just realized that make test by itself would fail (or use an out-of-date fstar.exe) since it doesn't depend on any build target. That's really unexpected.

Another options is to have test-1 and test-2 targets, and maybe test: test-2 for convenience. (Then the tests could also use different cache directories for each stage if we want to support that.)

I changed the rules to roughly do this (see last patch). I kept a make _test available that will just use the latest one, since I think I will be running this often when working with a stage 1 (to avoid the overhead of dune realizing there's nothing to do).

Most users will not use these rules

What you're saying is that if you only ever call make, then this defaults to make 2 and you'll only ever get a symlink to stage 2, right?

Yes exactly.

Is there a target to build stage N without messing with the symlinks?

I added stage1 and stage2 to build the stages without setting the out/ link. The shortcuts 1 and 2 call the respective stage target and then set the link.

[gebner]

SGTM. Thank you!

[gebner]

These files (hand-written ML, F*, ulib, etc.) all show up in the git diff. Should we mark them as binaries like the checked in ML files?

[gebner]

When I run make stage1, it seems to use the old Z3:

❯ make stage1
  EXTRACT          STAGE 1 FSTARC-BARE
  BUILD            STAGE 1 FSTARC-BARE
  EXTRACT          STAGE 1 PLUGINS
  BUILD            STAGE 1 FSTARC
  EXTRACT          STAGE 1 LIB
   CHECK           Prims.fst
* Error 17 at /home/gebner.linux/fstar/ulib/Prims.fst(498,0-498,68):
  - Z3 solver not found.
  - Required version: 4.8.5
  - Please download version 4.8.5 of Z3 from
        https://github.com/Z3Prover/z3/releases
    and install it into your $PATH as 'z3-4.8.5'.


make[1]: *** [mk/lib.mk:107: /home/gebner.linux/fstar/stage1/ulib.checked/Prims.fst.checked] Error 1
make: *** [Makefile:98: 1.alib.src] Error 2

[gebner]

Thanks for the fix!

Next thing: make stage1 does not seem to use context pruning either.

[gebner]

Another weird thing: if I have a file Foo.fst in the root directory, then make stage1 will build and extract that. Is that intentional?

[mtzguido]

Ah thanks! That's a consequence of implicitly adding . to the include path, and using the 'automatic' dep analysis (no roots -> scan everything in the include path).

[gebner]

Suggested change

	SHELL=/bin/bash
	SHELL=bash

Is there a reason we need to hardcode the full path to bash here?

As you've observed, this doesn't work in nixpkgs. More problematically, it doesn't work on NixOS either (where you'd need to write make SHELL=bash everytime you call make..).

(EDIT: Changed my suggestion to keep the SHELL but set it to bash instead of the full path. I just realized that you added this because of Debian, which defaults to dash.)

[mtzguido]

I think there's no need for bash at all actually, pushed a patch.

[mtzguido]

Commented before seeing the edit, does something fail in dash? I think I was being too defensive by using bash since I had many complicated rules, but that logic has been pushed to some scripts (which do require bash, but the Makefile does not afaict).

[gebner]

I didn't try to build on Debian, I was just figuring out the reason why you put the SHELL= there in the first place.

If you've already removed all the bashisms from the Makefile, then we're good now.

[gebner]

I'm not sure where best to put this tip, but with the new symlink forest it is super useful to set search.followSymlinks to false in vscode. Otherwise, ctrl-shift-f will show you results from stage1/ulib, stage2/ulib, and the extracted ML code.

Alternatively, we could also add these directories to .ignore.

[mtzguido]

I added a macos build and a release workflow. Some minor points to figure out are:

• Windows build: can we use cloud runners? I think this would be a lot more convenient that keeping a self-hosted one.
• Shape of binary package: it's currently slightly different (no fstar/ top level directory, just extracts bin/ and lib/ into the cwd, and it's not including license/version files --- I'll change it to the previous shape but comments welcome)
• Nightly builds: I have a workflow to create run a nightly build and push it to a 'nightly' release (which can have its artifacts updated) and a script to download the latest build. The one wart is that think we shouldn't force update a nightly tag, so the release's commit will not match the commit at which the artifacts were built. Or we can force the tag... (https://github.com/mtzguido/FStar/releases/tag/nightly)
• For Pulse: if we include the compiler's checked files into the package, we remove the need of having an FSTAR_HOME pointing to a repo, and could just off a package (nightly build?).

[gebner]

There seem to be some missing dependencies. If you switch between this PR and the gebner_smt_univs branch, then some (?) parts of the stage2 build don't seem to be rebuilt correctly:

git checkout mtzguido/dev
make -j`nproc` stage2
git checkout gebner_smt_univs
make -j`nproc` stage2
# lots of error messages that result from mixing old and new SMT encoding

It works after a git clean -fdx stage2 though.

[gebner]

Another QoL issue. Could we rename the executable to fstar.exe? The top output is very uninformative.

    PID USER      PR  NI    VIRT    RES    SHR S  %CPU  %MEM     TIME+ COMMAND
1842139 gebner    20   0  451248 433900  26632 R 100.0   0.7   0:20.26 main.exe
1842171 gebner    20   0  420076 398812  26900 R 100.0   0.6   0:18.73 main.exe
1842341 gebner    20   0  287160 259488  26552 R 100.0   0.4   0:11.47 main.exe
1842359 gebner    20   0  385040 367076  27072 R 100.0   0.6   0:10.80 main.exe
1842413 gebner    20   0  355708 317476  26724 R 100.0   0.5   0:08.53 main.exe
1842424 gebner    20   0  288460 256852  27080 R 100.0   0.4   0:07.91 main.exe
1842447 gebner    20   0  292596 257944  26344 R 100.0   0.4   0:06.21 main.exe
1842465 gebner    20   0  287220 249220  26184 R 100.0   0.4   0:05.82 main.exe
1842474 gebner    20   0  288448 255120  26372 R 100.0   0.4   0:03.92 main.exe
1842476 gebner    20   0  287160 240988  26380 R 100.0   0.4   0:03.90 main.exe
1842486 gebner    20   0  255200 215204  26416 R 100.0   0.3   0:03.52 main.exe
1842493 gebner    20   0  220576 172884  26356 R 100.0   0.3   0:02.98 main.exe
1842501 gebner    20   0  187480 165948  26228 R 100.0   0.3   0:02.83 main.exe
1842502 gebner    20   0  255520 211036  26608 R 100.0   0.3   0:02.83 main.exe
1842503 gebner    20   0  254444 210716  26312 R 100.0   0.3   0:02.79 main.exe
1842505 gebner    20   0  221160 199004  26560 R 100.0   0.3   0:02.74 main.exe
1842514 gebner    20   0  157384 133484  26208 R 100.0   0.2   0:02.46 main.exe
1842519 gebner    20   0  188368 146688  26516 R 100.0   0.2   0:02.36 main.exe
1842524 gebner    20   0  188816 141976  26520 R 100.0   0.2   0:01.92 main.exe
1842536 gebner    20   0  126916  96616  26536 R 100.0   0.1   0:01.33 main.exe
1842409 gebner    20   0  287420 250520  26304 R  90.0   0.4   0:08.68 main.exe

[mtzguido]

There seem to be some missing dependencies. If you switch between this PR and the gebner_smt_univs branch, then some (?) parts of the stage2 build don't seem to be rebuilt correctly:

git checkout mtzguido/dev
make -j`nproc` stage2
git checkout gebner_smt_univs
make -j`nproc` stage2
# lots of error messages that result from mixing old and new SMT encoding

It works after a git clean -fdx stage2 though.

I think the missing dependency is these checked files depending on fstar.exe, but adding it means every checked file would be invalidated by a tiny edit to the sources (like adding a debug line).

For changes that affect the contents of checked files we usually bump the version number in in Prims.fst and FStarC.CheckedFiles. Touching prims will force rebuilds. If you add a change like this to that branch does everything work fine?

[gebner]

I think the missing dependency is these checked files depending on fstar.exe, but adding it means every checked file would be invalidated by a tiny edit to the sources (like adding a debug line).

That sounds practical. Thank you for the explanation. With the missing dependency you can safely edit any .fst file and it will only be built twice, but it won't cause a full rebuild. It's something to keep in mind though.

For changes that affect the contents of checked files we usually bump the version number in in Prims.fst and FStarC.CheckedFiles. Touching prims will force rebuilds. If you add a change like this to that branch does everything work fine?

Yes, I could touch Prims.fst on every single commit but then stage1 would get rebuilt too which I want to avoid.

[gebner]

@mtzguido Thanks for renaming the executable to fstarc1_full.exe. Can you please update the vscode configs as well?