Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Heapster tutorial's build instructions are broken #1822

Closed
scuellar opened this issue Feb 14, 2023 · 2 comments
Closed

Heapster tutorial's build instructions are broken #1822

scuellar opened this issue Feb 14, 2023 · 2 comments
Assignees
Labels
subsystem: heapster Issues specifically related to memory verification using Heapster

Comments

@scuellar
Copy link
Collaborator

Probably after commit d2d9f01ce960209838f02af27a75d2d628e4094b the heapster build needs more specific instructions on building coq.

Specifically, it requires a particular version of EnTree.

@scuellar scuellar added the subsystem: heapster Issues specifically related to memory verification using Heapster label Feb 14, 2023
@scuellar scuellar self-assigned this Feb 14, 2023
@RyanGlScott
Copy link
Contributor

My bad, I forgot to update the tutorial when writing #1778. It should just be a matter of this part of the saw-core-coq README:

The recommended way to install Coq and these dependencies is using opam. This
can be done with the following steps, which will not only install opam, Coq, and
the above mentioned Coq libraries, but will make sure to install the proper
version of Coq needed for those libraries:
```
sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)
opam init
opam repo add coq-released https://coq.inria.fr/opam/released
opam install -y coq-bits
opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#52c4868f1f65c7ce74e90000214de27e23ba98fb
```

@scuellar
Copy link
Collaborator Author

Actually, I now realized the tutorial is fine. It points to that README correctly, I just had the wrong version of 'entree-specs'.

I'm closing this issue.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: heapster Issues specifically related to memory verification using Heapster
Projects
None yet
Development

When branches are created from issues, their pull requests are automatically linked.

2 participants