[isabelle-dev] Failure of AFP/Proof_Strategy_Language

Makarius makarius at sketis.net
Sat Oct 26 22:03:50 CEST 2024


In Isabelle/d3c0734059ee + AFP/4082096ade5a we have a failure of 
AFP/Proof_Strategy_Language:

Proof_Strategy_Language FAILED (see also "isabelle build_log -H Error 
Proof_Strategy_Language")
*** empty sequence. no proof found.
*** At command "find_proof" (line 88 of 
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 34 of 
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 101 of 
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 16 of 
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 29 of 
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 22 of 
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")


The parent Isabelle/0c9075bdff38 appears to be fine, so it is probably due to 
the changes in Sledgehammer in d3c0734059ee.


	Makarius


More information about the isabelle-dev mailing list