ulib dependencies not working well
- 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
Assessment
This issue has not been assessed yet.