everest: bootstrap F*, now required for building Pulse

[mtzguido]

Pulse relies on checked files for internal compiler modules, after FStarLang/pulse#246.

We use to avoid this need by keeping an OCaml snapshot of the checker in the Pulse repo, but we've removed that since. That was not ideal due to merge conflicts and etc, but also meant that an everest build would not check that Pulse can successfully build.

This changes the F* build rule to add the bootstrapping step.

--

This means an everest build will now be a bit slower. I am also wondering if we still want Pulse in the everest set of projects.

cc @tahina-pro @gebner @msprotz

[msprotz]

Thanks for the FYI. No objection on my part. As to the duration of the Everest build: build times have been slowly creeping upwards over time, so I don't think this is going to be a dealbreaker.

Keeping pulse in everest is mostly a question of whether check-world supersedes Everest. What's the status there? The most recent build was a month ago, so is the ambition still that check-world becomes a better version of the everest script? Do we then remove the build logic from everest, or do we keep it as a convenient way to do local regressions?

Cheers

[mtzguido]

Keeping pulse in everest is mostly a question of whether check-world supersedes Everest. What's the status there? The most recent build was a month ago, so is the ambition still that check-world becomes a better version of the everest script? Do we then remove the build logic from everest, or do we keep it as a convenient way to do local regressions?

I've been making progress in this F* PR FStarLang/FStar#3637, and running check-world there (https://github.com/mtzguido/FStar/actions/workflows/ci.yml, some of the runs have "friends" enabled, like https://github.com/mtzguido/FStar/actions/runs/12520179032). So yes I think that will be the way to do regression testing across projects.

I think there's still value in the everest script... I wouldn't mind keeping it working including Pulse.