[isabelle-dev] Failure of AFP/Proof_Strategy_Language

[Fabian Huch]

On 10/28/24 10:59, Peter Lammich wrote:
>
>
> 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?
>
It looks like the entry uses the API, but then prints the output and 
re-parses it (instead of working with typed data), which is of course bad.


Fabian