search

spechub / Hets

The Heterogeneous Tool Set
http://hets.eu
GNU General Public License v2.0
57 stars 19 forks source link

THF's input file for LeoII is always the same #1555

Open eugenk opened 8 years ago

eugenk commented 8 years ago

When Hets executes LeoII to prove a theorem, it always puts the input for LeoII at the same path, which is $PWD/_thm.p.

Running multiple instances of Hets in parallel, this file gets overwritten while LeoII is reading it. As a consequence, LeoII encounters syntax errors.

sternk commented 8 years ago

So simply placing it in a temp file should fix this?

eugenk commented 8 years ago

If the tempfile comes from the OS, then it should fix this. We need to ensure that there's always a different filepath.

cmaeder commented 8 years ago

I think for other provers we generated a name from the theory and the goal(s).

sternk commented 8 years ago

That seems sensible. Which one is preferable? & Do you maybe have an example?

eugenk commented 8 years ago

I'd mix those two methods: request a tempfile from the OS with a reference to the theory in the name (and the correct file extension). It should be located in the $TMPDIR

cmaeder commented 8 years ago

I think for "-o th" or "-o tptp" we got reasonable names

sternk commented 8 years ago

@eugenk: What would be the point in mixing these? The temporary file is unique and is never used by anyone else (and should be deleted after the proof)

eugenk commented 8 years ago

For debugging purposes ;) Sometimes it comes in handy when you debug something and you are sure that you got the right file.

sternk commented 8 years ago

So we'd want to mimick https://github.com/spechub/Hets/blob/master/Driver/WriteFn.hs#L211 + random component?

cmaeder commented 8 years ago

For darwin SoftFOL/ProveDarwin.hs only the theory name is used as a base name for the temp file