[isabelle-dev] clang error

Makarius makarius at sketis.net
Wed Jul 24 23:30:26 CEST 2024


On 7/24/24 20:23, Norbert Schirmer wrote:
> 
>> On 24. Jul 2024, at 16:15, Norbert Schirmer <nschirmer at apple.com> wrote:
>>
>> There is at least one commit in the development version that could 
>> have changed the behaviour:
>> https://isabelle-dev.sketis.net/ 
>> rAFPb626e627c3cb280b4fb609d9ebebe1e905930f83

> I have meanwhile confirmed on my machine that this is actually the 
> changeset that introduces the problem.

I have stared at that for a long time, and then produced this one:

changeset:   14716:77cb7384c8df
tag:         tip
user:        wenzelm
date:        Wed Jul 24 22:59:02 2024 +0200
summary:     avoid spurious whitespace for the sake of cpp on macOS 
(amending b626e627c3cb);

In other words "cpp -I xyz" is different from "cpp -Ixyz" on macOS: 
really strange, but such things happen.


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


(That is on Isabelle/49b38572a9f1.)


	Makarius



More information about the isabelle-dev mailing list