generate corrupted .olean file even if compilation fails

[leodemoura]

No description provided.

[leodemoura]

I added --permissive option to lean.
It produces the .olean file even when errors are detected.
We can use it to implement a solution for the flycheck problem reported by Jeremy.
The idea would be to make lmake to create an auxiliary file (e.g., .lmake_opts) that stores the configuration options used.
All .olean files would depend on it. So, if the file is modified, we are forced to recompile all .olean files.
flycheck would use the --permissive, and the lean main makefile would not.

[soonhokong]

All .olean files would depend on it

I wanted not to change makefile.common so I add the following things to lmake:

• lmake creates .lean_options file where a makefile is located.
• Whenever lmake is executed, it update .lean_options file.
• If lmake detects a change in .lean_options file, it touches all the .lean files under the root of makefile. This will force make to recompile .lean files.

[leodemoura]

I think this is a good solution

[soonhokong]

It turns out that these "touches" are the root of 'file changed on disk' emacs messages. I'm changing things to use the following option for make in lmake if there is a change in lean option.

  -B, --always-make           Unconditionally make all targets.