Proof failed but Holmake doesn't report it

[binghe]

Proof failed but Holmake doesn't report it

[mn200]

My suspicion is that while the output isn't being hidden, the corresponding exception is being caught in the code. Look for example at the body of COMB_SYNTH_CONV in compile.sml. That code should be adjusted not to call the high-level prove function, but to instead use TAC_PROOF or similar. This would make the process quieter.

[mn200]

Have fixed the real problem.

[binghe]

I think HOL builds are still randomly failing at the same theory.

[mn200]

That's probably a Poly/ML issue: I've stopped the unnecessary printing of exception messages caused by proofs failing.

[binghe]

That's probably a Poly/ML issue: I've stopped the unnecessary printing of exception messages caused by proofs failing.

I use PolyML master in my local computer. Let's also switch to it (from 5.9.1) for the Docker image and see what happens.

[binghe]

Now I see what's happening (next): with lastest Poly/ML master HOL session crashed: