Andreas Lööw

Holmake -k fails if Holdep fails

4

Consider the following Holmake invocation: ``` > Holmake -k Working in $(HOLDIR)/examples/balanced_bst [...] Working in . Holdep failed: tinyMachineScript.sml 469.66 Unescaped newline in string literal Holmake failed with exception: HolDepFailed...

Unexpected behaviour of specialize with (...:=...) in combination with typeclasses

1

#### Description of the problem Hi, can the following be considered a bug? I expected both `specialize` invocations to work the same here. ```coq Class Foo A := { foo...

Coerced ports not reflected in JSON output

4

I don't know if this is the intended behaviour or not, but the following module: ``` module foo(input a); assign a = 1; endmodule ``` generates the following warnings: ```...

Proof General UI and kernel out of sync from aborting tactics?

2

Hi, there seems to be some problems with aborting some of the tactics provided by CoqHammer. To exemplify, consider this proof script (just some function and a theorem from the...

UI and kernel out of sync from aborting tactics?

1

Hi, it seems that aborting long-running tactics (using C-c C-c) can cause the UI and kernel to go out of sync. I have noticed this with CoqHammer's tactics specifically, e.g....