Unable to set Coq properties

[arnoudvanderleer]

When I try to configure coq properties, following the last two lines of the documentation, I get an exception:

Anomaly ""Assert_failure _vendor+v8.16+32bit/coq/library/lib.ml:169:57"."
Please report at http://coq.inria.fr/bugs/.
Anomaly "Uncaught exception Option.IsNone."
Please report at http://coq.inria.fr/bugs/.

With this in the js console:

(This is the default examples/scatchpad.html, to which I added the option coq: {'Implicit Arguments': true, 'Default Timeout': 10})

[corwin-of-amber]

@ejgallego I think you mentioned this at some point and had an idea of why it might pop up?

[arnoudvanderleer]

(See also the corresponding discussion on the zulip)

[ejgallego]

Yes, this was broken in some migration, Coq init routine is different so we need to tweak the code that fixes this.

It should not be hard, basically the options need now to be set at document creation time using the Stm.new_doc API. Before Coq 8.16 you were expected to set up the options before the document creation time. This is what now triggers the assertion.

I won't have time to look at this until next week due to holidays, feel free to write the patch yourselves.

In particular, you should put the options in the injections options here: https://github.com/coq/coq/blob/v8.16/stm/stm.mli#L60