[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