Comments (2)
mansky1
commented on June 22, 2024
I looked into this, and I think it's a bitsize issue. By default VST is set up for 64-bit programs, but the progs examples are 32-bit. This mostly doesn't change the proofs (as you can tell from the fact that you got that far), but something seems to get stuck at the very end. If you try the same thing in the progs64 folder, it should work completely.
from vst.
eleehiga
commented on June 22, 2024
@mansky1 Thank you the progs64 version worked completely. Perhaps you guys should note somewhere that people should run the tutorials from the progs64 folder.
from vst.
Related Issues (20)
- Please create a tag for Coq 8.18 in Coq Platform 2023.10 HOT 5
- Some observations on `forward_call` performance HOT 21
- Useful lemma for users: nonempty_writable_glb
- do {S} while (0)
- Unnecessary premise in `Lemma field_at_app`
- fail levels in forward_if'_new
- overbroad match in try_conjuncts
- Function pointer comparison apparently not supported
- solve_load_rule_evaluation @proj_reptype HOT 3
- data_at_int_or_ptr_int share
- forward_call takes a long time HOT 2
- Improvements in deadvars
- solve_store_rule_evaluation HOT 1
- localize / entailer_for_load_tac / unlocalize / Coq 8.17 HOT 11
- Please create a tag for Coq 8.19 in Coq Platform 2024.01 HOT 4
- inhabited_value doesn't really work well
- mkVSU external function check does not give useful error message HOT 3
- cstring should not need a compspecs argument HOT 2
- verif_incr should prove that it restores an uninitialized counter HOT 1
- IPM proof fails in lib/proof body_release, succeeds in atomics body_release HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from vst.