Use .hpf proof script files for batch testing

[maeder]

hets Calculi/Space/RCCVerification.hpf

finally fails with:

Goal cmps_NTPPiNTPP is proved.

Goal cmps_NTPPiTPPi is still open.

Goal cmps_NTPPiNTPPi is proved.

Analyzing node ExtRCCByRCC8Rels_E1

Goal cmps_DCEC is still open.

Analyzing node ExtRCCByRCC8Rels_E1

Goal DR_eq_DC_or_EC is still open.

Analyzing node ExtRCCByRCC8Rels_E1

Goal DR_eq_DC_or_EC is still open.

Analyzing node ExtRCCByRCC8Rels_E1

Goal DR_eq_DC_or_EC is still open.

Adding comorphism
The following error(s) occured :
No applicable prover with this name found
Analyzing node RCC_FO_in_MetricSpace_T
hets: user error (Proofs.InferBasic: no matching known prover)
Prover stopped.
Analyzing node RCC_FO_in_MetricSpace_T
hets: user error (Proofs.InferBasic: no matching known prover)
Prover stopped.

Also goals should not remain open when replaying them (Hets-lib revision 1146, Hets 11594)

[maeder]

It seems only Isabelle is not supported. Another problem that I have is with running in the background. In many cases the jobs do not proceed:

[1]+  Running                 hets Datatypes.hpf >&log &

It looks as if SPASS does not start or return.

[mgross]

Replying to maeder:

Another problem that I have is with running in the background. In many cases the jobs do not proceed ... It looks as if SPASS does not start or return.

This works for me...

[1]  + done       hets Datatypes.hpf >&log &

[maeder]

Indeed,

hets -v2 Basic/[A-MR-S]*.hpf >& log

worked too, but leaves many

The following error(s) occured :

messages, that need to be corrected.

(Excluding the example file Basic/Numbers.hpf is also a pain.) Could you correct the other Basic/*.hpf files, Markus?

[maeder]

I think, most errors are due to changed names (of unnamed nodes)

[till]

Replying to maeder:

I think, most errors are due to changed names (of unnamed nodes)

We should implement a unique naming scheme. Are the errors due to a lack of unique naming scheme, or has the problem been that the unique naming scheme changed at some point?

[maeder]

The unique naming scheme changed by implementing #729 and changes of source:trunk/Static/AnalysisStructured.hs

[maeder]

It's best to use "Edit-> Focus node" of hets-0.93 and a current hets to see how names have changed. (Extensions E3 ... E1 are now number E1 ... E3, VectorTuple_1E3A is now VectorTuple_RE1TA1.)

[mgross]

The Basic/*.hpf files are corrected in Hets-lib rev 1287.

[maeder]

Good, could you also check the Calculi/*/*.hpf files? (For Isabelle proof scripts we need another ticket.)

[mgross]

All hpf files are now adjusted to the new naming scheme.

[maeder]

on gemini batch testing gets stuck on the first file

 -      (06116)   21148 sh sh sh
 -       |        21149 /bin/bash -x /local/home/maeder/haskell/cronjob.sh
 -        |       26572 ./hets -v2 Datatypes.hpf
 -         |      26573 ./hets -v2 Datatypes.hpf
 -      (06116)   24456 sh sh sh
 -       |        24457 /bin/bash -x /local/home/maeder/haskell/cronjob.sh
 -        |       29951 ./hets -v2 Datatypes.hpf
 -         |      29952 ./hets -v2 Datatypes.hpf

[maeder]

today, everything went through, so let's wait for a reproducible problem