[isabelle-dev] clang error

[Norbert Schirmer]

> On 25. Jul 2024, at 00:04, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
> So now the call to 
> 
>> install_C_file "word_abs.c"
>> autocorres
>>  [ (* signed_word_abs is implicit; these are the functions that would be abstracted: *)
>>    (*signed_word_abs =
>>        S_add_S S_sub_S S_mul_S S_div_S S_mod_S neg_S
>> ...  , ts_rules = nondet
>> ] “word_abs.c”
> 
> in AutoCorres2/tests/examples/WordAbs.thy turns purple and hangs, apparently without doing any work.
> 
> Larry
> 

The Ramsey commit in Isabelle broke that proof. See here.

changeset:   14717:a4c2d293808e
tag:         tip
user:        Norbert Schirmer <nschirmer at apple.com>
date:        Thu Jul 25 09:37:11 2024 +0200
summary:     fix proof following Isabelle/e65eed943bee

Regards,
Norbert

--

Norbert Schirmer (nschirmer at apple.com)
 SEG Formal Verification






-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240725/7b51408b/attachment.htm>