[isabelle-dev] clang error

Lawrence Paulson lp15 at cam.ac.uk
Thu Jul 25 00:04:04 CEST 2024


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

> On 24 Jul 2024, at 22:30, Makarius <makarius at sketis.net> wrote:
> 
> Now there is a new problem on that machine:
> 
> isabelle build -d '$AFP' -D thys/AutoCorres2/
> Running AutoCorres2_Test ...
> Warning - Unable to increase stack - interrupting thread
> AutoCorres2_Test FAILED (see also "isabelle build_log -H Error AutoCorres2_Test")
> *** exception Interrupt_Breakdown raised
> *** At command "by" (line 361 of "$AFP/AutoCorres2/tests/examples/WordAbs.thy")
> Unfinished session(s): AutoCorres2_Test
> 



More information about the isabelle-dev mailing list