William Mansky
William Mansky
Last time I talked to @lennartberinger about this axiom he said it should be true, but it's more of a sanity check than a rule of the logic, and could...
You shouldn't need to run `make` to start running examples, although you may encounter problems if you both install VST through OPAM and also try to clone the repo and...
Once VST is installed through OPAM (and you're using the OPAM version of Coq/CoqIDE), if you just open the files and start running them, they should work. Depending on the...
If I correctly understand the situation, the error with the includes was because you were running CoqIde from Snap and trying to load VST from OPAM. Once you uninstall the...
This depends on a dev version of Iris from `iris-dev`, so it can't currently pass the CI. Does that mean we need to host it through `iris-dev` rather than here?
There's some kind of issue with the path to the git submodule. I'll do some debugging and see why it works in our CI but not in opam.
Okay, it should be ready!
Oh, interesting! I'll try a few approaches. I also noticed that they've finally included "Disable Notation", which might help with some of the map notation clashes.
There were two problems here: 1) the definition that was being destructed was declared `Opaque`, and 2) the `Timeless` instance for `atomic_int_at` wasn't declared as an instance. It should work...
@andrew-appel I'm now working on getting this to pass the CI -- it currently works only for 8.17 and 64-bit mode. Which Coq versions and bitsizes does it need to...