Provide a convenient way to run examples with OPAM-install VST

[QinshiWang]

A VST user runs into issue #614. I think he wants to install VST and run some examples. In order to run the examples, he needs to first make. But make in VST repo should be making VST from source code. Maybe it is worth improving the user experience.

[eleehiga]

@QinshiWang Is it that make in the VST repo is making VST from coq-vst and not the source code currently?

[QinshiWang]

make is making from source code, not from OPAM.

[mansky1]

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 compile the examples. Maybe we need to write instructions for checking out and compiling just the examples against an OPAM version of VST.

[eleehiga]

@mansky1 That sounds good and how do I run the VST examples for the OPAM version of VST?

[mansky1]

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 example, you may need to run clightgen on the .c file first.

[eleehiga]

Ah ok I understand, I remember though when I was trying to run verif_sumarray.v from the VST source that there was an error with the includes and I thought to get rid of those that I had to run make. Therefore, was wondering how you would recommend me to rid of those include errors without running make?

[mansky1]

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 Snap package and/or run CoqIde from OPAM, that error should disappear. If it doesn't, we can investigate further. (It should also be possible to uninstall the OPAM version of Coq and make VST from scratch with the Snap version, but that's not the subject of this issue.)

[eleehiga]

Ok that all sounds good and I will try run Coq and VST from OPAM

[eleehiga]

Also, for your guys' installation instructions you guys should specify to install the OPAM version and not the Snap version of Coq

[andrew-appel]

@eleehiga Specifically, do you recommend adding the line with the # comment to the BUILD_ORGANIZATION.md file?

Install Method 2: use opam directly

If you install VST via opam, opam will try to install a
suitable version of CompCert, Flocq and other dependencies.
  opam install coq  # best to install coq by opam instead of some other method
  opam install coq-vst
  AND/OR
  opam install coq-vst-64