[isabelle-dev] clang error

[Makarius]

On 7/25/24 10:00, Norbert Schirmer wrote:
> 
>> On 24. Jul 2024, at 23:36, Makarius <makarius at sketis.net> wrote:
>>
>> The in-theory config option does not quite make sense to me: it needs 
>> to be configured in the system context, not the theory context. So 
>> that attribute could just disappear, unless there are odd reasons to 
>> keep it. (Many things in AutoCorres2 are odd.)
> 
> 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.

AutoCorres2 has a lot of adhoc options and even unsynchronized program 
variables: often these are plain wrong in terms of parallel Isabelle/ML.

Further there are situations were source files are changed in the 
file-system, where normally something like session exports and/or 
generated_files are used. It will require a long time to migrate the 
codebase from 15-20 years ago into the present.


	Makarius