FStarLang / FStarLang/FStar

ulib dependencies not working well

Open
#1,978 5 comments 0 reactions 1 assignee Claimed by @mtzguido View on GitHub
component/build kind/bug kind/discussion
Dominant language
F*
Stars
3.1k
Forks
266
Avg merge
21h 1m
Merged PRs (30d)
54

Description

Something is wrong with our makefile here (and has been for a long while, trying to find when exactly it regressed).

Start from a clean build and build `FStar.Squash.fst.checked` like so
```
fstar/ulib/$ make -C ../ 1 -j4 && FSTAR_HOME=.. make -j4 -f Makefile.verify V=1 .cache/FStar.Squash.fst.checked
(depend...)
...
/home/guido/r/fstar/master/bin/fstar.exe --use_extracted_interfaces true --warn_error -271 --use_hints --cache_dir .cache --hint_dir .cache --cache_checked_modules --odir _output FStar.Squash.fst
Verified module: FStar.Squash
All verification conditions discharged successfully
```

Now touch `FStar.Squash.fst`, or even modify it as long as you don't introduce a syntax error, and run the makefile again:
```
$ touch FStar.Squash.fst
$ FSTAR_HOME=.. make -j4 -f Makefile.verify V=1 .cache/FStar.Squash.fst.checked
(depend...)
make: '.cache/FStar.Squash.fst.checked' is up to date.
```

This predates the new silent makefile and all that.

-----

Also, separate issue: our use of `touch -c` for updating the timestamp is wrong. Suppose `B.fst` depends on `A.fst`, and suppose both checked files are stale. Also that we are building `B.fst.checked ` without updating `A.fst.checked` (which should NOT happen, that's the bug above, but imagine). Then F* will run on `B.fst` but not save the checked file, since it detects `A.fst.checked` is stale and does nothing. Then we touch `B.fst.checked` and make it seem like it did, and we're now in a very crappy state.

Again, we should never reach this second circumstance, but let's avoid `touch -c` since it can lead to weird stuff like this. We could make F* itself update the timestamp.

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.