[isabelle-dev] clang error

[Achim D. Brucker]

Hi,

> > One use case is to configure a cpp script there that does some
> > additional checks before invoking the actual cpp. Typically a per
> > session setting would be enough, but in general there could be multiple
> > “install_C_file” commands in one session that want to use different
> > settings.
> 
> That is a bit odd, but sufficient proof to leave the config option there.


I guess this is a somewhat tricky question to decide which way is the
"gold standard". From my (limited) experience with working with
AutoCorres, I see two different scenarios:

1) When working on smaller examples that are generic and expected to
   work on various compilers / operating systems without any
   additional installation setting for "proof engineers". In this
   scenario, a global setting (not even session specific) would be
   nice. Otherwise we needed at least for some cases the wrapper
   script that ensures that the clang cpp on MacOS behaves more
   like GNU cpp on Linux/Cygwin. 

2) When working with "real world" examples, the C-compiler toolchain
   needs to be fixed anyway for all people working on the AutoCorres
   theories for reasons outside of AutoCorres (e.g., embedded C
   toolchains can be finicky about versions and setups on their
   own). In this case, it can be useful to have it as "theory-level"
   configuration option.

I guess, 1) is a more educational/teaching scenario (e.g., using
AutoCorres for student projects, where I priotise a nice "out of the
box expierence" over "on every machine raelly the exact same output
from cpp is generated" ) and 2) is the more "real-world" scenario.

Cheers,
        Achim