[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