[isabelle-dev] clang error

Makarius makarius at sketis.net
Wed Jul 24 11:47:03 CEST 2024


On 7/24/24 10:52, Lawrence Paulson wrote:
> I’m trying to figure out why AutoCorres2 doesn’t terminate in text/examples/WordAbs. But the first thing I get is
> 
> install C file
> 2.864s elapsed time, 0.384s cpu time, 0.000s GC time
> clang: error: no such file or directory: 'c'
> clang: warning: /tmp/isabelle-lp15/process637078695862628399/cpp14274848: 'linker' input unused [-Wunused-command-line-argument]

I also see this on the nightly build "AFP (macOS 14 Sonoma, Apple 
Silicon)", see https://isatest.sketis.net/devel/build_status/index.html

It is unclear to me what it means. The AutoCorres2 guys are at home on 
the macOS platform, so they should be able to say more.


As usual, Linux should work without problems --- and Windows/Cygwin, 
too, after I've spent 1-2 weeks to tinker on it.

Generally, AutoCorres2 has many rough edges, which are to be sorted out 
soon: Now that it is in AFP it will be subject to the "automagic 
maintenance" of that environment.


	Makarius



More information about the isabelle-dev mailing list