search

spechub / Hets

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

Prover Isabelle is not supported in CMDL mode #736

Open sternk opened 10 years ago

sternk commented 10 years ago

Reported by maeder and assigned to ldiaconu Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/736

hets Calculi/Space/RCCVerification.hpf

fails with

> dg basic RCC_FO_in_MetricSpace_T                         
> translate HasCASL2IsabelleBoolPair                       
The following error(s) occured :                           
Wrong comorphism name                                      
> prover Isabelle                                          
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)

The Isabelle proof script is also ignored. Have there been any thoughts yet, how the proof script should be merged into a Isabelle theory? (I should be able to run Isabelle in batch mode, which is related to #158) I'm going to move this .hpf file out of the way to allow batch testing the other .hpf files.

sternk commented 10 years ago

Comment by till Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/736#comment:1

Replying to maeder:

The Isabelle proof script is also ignored. Have there been any thoughts yet, how the proof script should be merged into a Isabelle theory? (I should be able to run Isabelle in batch mode, which is related to #158)

For the interactive mode, this will be done by the new broker. Perhaps this also works for batch processing of heterogeneous scripts.