Karl Palmskog

Update for Dune-Coq 0.8 and Coq 8.17

4

Experiment with Dune-Coq 0.8 using docker-coq-action CI.

This is the designated place to suggest and discuss additional mutation operators. Catalin Hritcu has already suggested a mutation operator based on _removing_ constructors of inductive types.

We should document the available mutation operators somewhere in the repository, preferably with examples of how they affect Coq code. Most directly, we could add a file `OPERATORS.md` and list...

add basic meta.yml, generate README.md from templates

5

Rather than ad-hoc updating README.md, how about using `meta.yml` @yforster? This is the closest I can get to the current README.md.

IndexError: list index out of range

1

I get this when I try to get suggestions for the file [wmso.v](https://github.com/coq-community/reglang/blob/master/theories/wmso.v) in the [RegLang](https://github.com/coq-community/reglang) project: ```shell $ python -m roosterize.main suggest_lemmas --project=../reglang --serapi-options="-Q theories,RegLang" --model-dir=./models/roosterize-ta --output=./output >>>>> Extracting...

Right now, when Roosterize suggests lemma names for a complete project, that project has to be built first (usually using `make` in it root directory). However, it would be more...

I don't see any indication of a license for this project. Since the functions verified are inherently general and useful, it would enable others to reuse them if there was...

### Is your feature request related to a problem? Currently, Coq extraction does not support functions with nontrivial sort polymorphism (instantiations using `Prop` or `SProp`), as can be seen in...

Extracting functions using have tactic fails in Coq 8.20 and later

12

### Description of the problem In Coq 8.20 and later, functions that (somewhere) use SSReflect's `have` tactic opaquely (the standard use which means using `ssr_have_upoly`) cannot be extracted, and fail...