V2.1.0

[aleksnanevski]

• A new minor release to support Hierarchy Builder 1.8 and coq-fcsl-pcm v2.1.0
• Added lemma for backward symbolic execution (bnd_vrf) in htt/model.v
• Added makefiles to build packages (suggested by Karl Palmskog).

[aleksnanevski]

@palmskog Hi Karl. I implemented the changes that you recommended yesterday, I think. Before I merge, would you please mind checking if I did so correctly, and if the setup will correctly package the files.

[palmskog]

Looks good to me, but why remove Dune-related files? There is no harm in keeping them around, and it gives more options what do with the release, e.g., use Dune locally.

[aleksnanevski]

Hm, ok, I can try to put the dune back. The first few attempts to build have failed, so I erased the dune files because I was unsure as to how they work. The error ended up being elsewhere in the end.

[aleksnanevski]

@palmskog Hmm, I'm having a problem with using the package, and I wonder if it has to do with the change in the build. Once I install coq-htt-core and coq-htt, the system, for some reason, doesn't assign them logical names. So I can't import the files into other projects. The behavior is different in fcsl-pcm, which does receive a logical name. Have you experienced this before?

[palmskog]

@aleksnanevski the only difference I can see is that the package build now uses -Q - all the files are getting installed and so on, and the files are there in user-contrib/htt after installation. For example, the following command works fine in both htt 2.0.1 and 2.1.0:

From htt Require Import quicksort options.

[aleksnanevski]

Yes, the problem was that I just didn't refresh the opam environment variables via eval $(opam env). Sorry for the false alarm.