[isabelle-dev] clang error

[Achim D. Brucker]

Hi,

For some versions of OS X it was possible (at least for AutoCorres as
available in the l4v repository on GitHub) to use a wrapper script for
cpp (attached, for reference) to ensure compatibility with GNU cpp.
If I recall it correctly, this was mostly needed for C files with
mixing define-macros one C-style comments and not using it resulted in
parsing errors (and not the directory not found error reported). 

Still, it might be worth a try to check if the error goes away when
using the attached script. This requires to configure the cpp_path:

declare[[cpp_path="/path/to/cpp"]]

Where cpp is the attached script.

Best,
        Achim 

On Wed, Jul 24, 2024 at 03:05:05PM GMT, Norbert Schirmer wrote:
> 
> > On 24. Jul 2024, at 11:47, Makarius <makarius at sketis.net> wrote:
> > 
> > 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.
> 
> Since when does this problem occur?
> 
> The “C-Parser” part of AutoCorres2 uses “cpp” to pre-process the input C programs. Isabelle/ML invokes this as a shell command. So I can imagine various issues:
> * cpp version not as expected (it is not bundled as a Isabelle-compnent, it just uses what is there)
> * Some processing of arguments of the shell command does not work as expected
> 
>   Regards,
> 
>   Norbert

> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
#!/bin/bash
#
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: BSD-2-Clause
#

#
# Wrapper for clang C preprocessor on MacOS
#
export L4CPP="-DTARGET=ARM -DTARGET_ARM -DPLATFORM=Sabre -DPLATFORM_Sabre"

if [[ "$OSTYPE" == "darwin"* ]]; then
    llvm-gcc -Wno-invalid-pp-token -E -x c $@
else
    cpp -Wno-invalid-pp-token -E -x c $@
fi