firstorder causes proof tree to hang

[emichael]

I can send you the code to repro the issue if you need it. htop shows minimal memory usage (out of 16GB) and 1 of 8 cores being used 100% on a single coqtop ideslave.

Even after the user clicks on another tactic in the tree, the server still hangs on trying firstorder.

[Ptival]

Is it a goal that should be solved immediately?

What happens under other Coq IDEs?

[emichael]

No, it shouldn't be solved. I'll try tomorrow, but I'm sure CoqIDE would
hang, too, if you actually tried to use firstorder.

The issue is that firstorder is only ever called because the proof tree is
looking at suggestions for the next tactic.

On Monday, November 9, 2015, Valentin Robert notifications@github.com
wrote:

Is it a goal that should be solved immediately?

What happens under other Coq IDEs?

—
Reply to this email directly or view it on GitHub
#26 (comment).

Ellis

[Ptival]

I see. In general it is indeed a bad idea to call firstorder without a timeout (or actually, all tactics).

I'll try to look into implementing a timeout safety, I believe there was a tactical for that.

[emichael]

In addition to a timeout, immediately halting all the tactics the proof tree is trying when the user selects a tactic might be a good idea.