imdea-software / htt Goto Github PK

1. m = m' + ms
2. tms = syntactify ms
3. tg = syntactify g
4. trs = subtract tg tms
5. r = pprint trs
6. partition m r

This forces us to bundle logical variables into one, so that they can be passed to gh_ex in a proof. model.gE from FCSL can accept multiple arguments by packaging them in a nested existential.

The README.md is missing:

• A better description of HTT,
• a pointer to HTT publications and/or,
• a pointer to Aleks @aleksnanevski's old website:

http://software.imdea.org/~aleks/htt/

Alternatively, we could replace Aleks website stub with a github.io-based website for the project.

I think most projects that use HTT can be expected to only use the framework parts (htt directory), as opposed to the examples. And while compiling htt takes a few seconds, examples seems to take around 3 minutes on a reasonably modern machine.

So to make it easier to depend on htt in a lightweight way, how about splitting off the examples into a separate coq-htt-examples package? Each package would be served from the same archive/release, but users can choose whether they want examples or not.

As one example, I split up the library and the tactic in Stalmarck with Dune.

• congmath.v
• congprog.v
• counter.v
• hashtab.v
• array.v
• queue.v
• stack.v

Possibly these as well:

• exploit.v
• llist.v

A continuation of #8.

The main roadblock with these two are the universe inconsistency issues.

The artifact at http://software.imdea.org/~aleks/htt/htt.zip contains some changes that aren't present in this repo.