engineeringsoftware / mcoq Goto Github PK

Hi folks, thanks for the tool, I liked it a lot.

To test a project of mine I had to disable the function detecting the JDK version.
I'm using macOS and openjdk package installed via Homebrew.

Here is what java -version command outputs on my system:

$ java -version 2>&1
openjdk version "11" 2018-09-25
OpenJDK Runtime Environment 18.9 (build 11+28)
OpenJDK 64-Bit Server VM 18.9 (build 11+28, mixed mode)

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.

I have a project I'd like to try mCoq on, but it does not build under anything < 8.11. Are there any plans to support Coq 8.11?

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 them all. This documentation could also be added to the inline help for mcoq.py.