WIP: load an options file everywhere to avoid repetition

Note that I didn't yet remove the "Set Default Proof Using" everywhere, this is just trying the general concept. Thanks to @janno for your help!

This fixes #66 (closed).

I just tried this for coq-std++, see https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/options, but I don't think it works for all options. In coq-std++ I have the following options file:

Generalizable All Variables.
Set Automatic Coercions Import.
Set Asymmetric Patterns.
Unset Transparent Obligations.
Obligation Tactic := idtac.

If I understand correctly, this file is ran at the top of the file before any Require commands. But that is wrong, it should be ran after the Require commands. The problem is that important another library (in this case, the standard library) could change these settings. In coq-std++ this this actually happens: Program changes Obligation Tactic.

I suppose this is also the reason you still have a:

Global Set Bullet Behavior "Strict Subproofs".

in theories/algebra/base.v because ssreflect would otherwise just change it.

By the way, note that this problem would not occur if no library we depend on would change such settings globally, but unfortunately that is not the case for ssreflect and the Coq standard library.

I suggest reporting these as bugs to Coq and ssreflect. Additionally, why not import ssreflect and Program in options.v? I know they are not options per se but one could argue that they might just as well be. (Who would be surprised if Coq made us write Set Program instead of Require Import Program ? Not me..)

I am not sure that this is a bug in either, it would be more of a feature request to organize such options in a better way.

Your suggestion about Require Import Program may work, will try.

I tried, but it makes coqc print stuff like:

R32:37 Coq.Program.Basics <> <> lib
R39:44 Coq.Program.Syntax <> <> lib

That seems like the output of the .glob file for the options file?

Ouch, that looks weird. coqdep will also not find files imported via Load as dependencies, I expect...

We could control when the file is loaded by using an explicit Load in the files instead of the -l option. The only trouble with this is, we could forget it, and then some files would not use the option.

Hm, I suppose I could write a CI job testing this...

Well, the explicit Load would be much like the original suggestion in #66 (closed). We could try to see whether that actually works, or whether there are other complications.

added 6 commits

• 16bffaa3...9c0c4620 - 5 commits from branch master
• 89681df8 - load an options file everywhere to avoid repetition

Compare with previous version

I did that, and updated this MR.

But ouch, lambdaRust can't load this file...

... but we can fix that with Makefile hackery, which I just added.

added 2 commits

• 3e35a2f1 - load an options file everywhere to avoid repetition
• 95c7b32b - hack Makefile to install .v files (for iris_options)

Compare with previous version

I don't really like the idea of loading a system-installed .v file from LambdaRust. Why LambdaRust would not have its own option file, duplicating most of Iris'? Actually, when you think about it, making LambdaRust use the very same file as Iris causes compatibility issues, since we do not want changes of Iris' options to contaminate other projects (otherwise, we would just have made them Global).

Given PMP's warning:

In the meanwhile, PLEASE DO NOT USE LOAD. Pardon the capitalizing, but that's important matter here. This command is a rather horrendous hack that SHOULD NOT appear in proper development files. It is borderline to use it in interactive proofs, and it should not be used anywhere else. I even think it is more or less bound to be removed at a future stage.

We should really reconsider whether we want to do this. It sounds like piling up a bunch of hacks on top of a hack. Not sure whether that's better than what we are currently doing.

As if you would never pile hacks upon hacks. ;)

I agree though there is no pressing need to do this right now. I'll keep the issue open (because we may want to solve this eventually), but close the MR.

closed