[isabelle-dev] Failure of AFP/Proof_Strategy_Language

[Peter Lammich]

On 28/10/2024 09:39, Jasmin Blanchette wrote:
> Hi Makarius,
>
> Yes, my (actually: Lukas Bartl's, under my supervision) change to 
> Sledgehammer (d3c0734059ee) is probably the issue.
>
> Sledgehammer is an end user tool. It should be possible to change its 
> output without breaking things. So I'm not a big fan of the 
> "Proof_Strategy_Language" entry's existence in the AFP. But since it's 
> there, maybe we could ask its developer to fix it?

Doesn't sledgehammer have an API?

--

   Peter


>
> Best,
> Jasmin
>
> --
> Prof. Dr. Jasmin Blanchette
> Chair of Theoretical Computer Science and Theorem Proving
> Ludwig-Maximilians-Universität München
> Oettingenstr. 67, 80538 München, Germany
> Tel.: +49 (0)89 2180 9341
> Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html
>
>
>> On 26. Oct 2024, at 22:03, Makarius <makarius at sketis.net> wrote:
>>
>> 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
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20241028/f5f43029/attachment-0001.htm>