Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Hi Christian,

Christian Doczkal 
<>
 writes:

> I would like to introduce a few colleagues to Coq/MathComp/Ssreflect and
> I'm looking for tutorials that I could use.
>
> I really like the JsCoq slides from the ITP 2016 Tutorial [1], but it
> seems these have fallen to some kind of bit-rot since then.
>
> In Lesson 1 (on Ubuntu 16.10+Chromium 59) I get various errors when
> trying to execute the search commands. Most often I get:
>>
>> Anomaly: Uncaught exception SyntaxError: Invalid regular expression:
> /maximum call stack/: Maximum call stack size exceeded. Please report.

I don't remember now if Chromium 59 was using the "ignition" js engine,
you may try to use the command line flag:

--js-flags="--harmony-tailcalls"

and see if that improves your problem, otherwise, enabling
chrome://flags/#enable-javascript-harmony may definitively help.

Let me know what the outcome was. Also, Firefox seems to work a bit
better some times.

>> Error: Unable to locate library all_algebra with prefix mathcomp.
>
> Is this some problem with my browser(s) or can this be remedied somehow?
> Failing that, what other Tutorials would you recommend to introduce
> people to MathComp?

I think this is a bug of the slides in that they don't enable the proper
package, try clicking on math-comp in the package manager (before
running any command) and that should work.

Most of these are problems of the jsCoq, unfortunately browser memory
performance has become a bit worse in the last Chrome releases.

Also, it would be good to update the jsCoq version used in the slides,
this is a trivial step.

I still believe that at some point the triple (Coq,js_of_ocaml,chrome)
will reach a state where it is feasible to use jsCoq seamlessly, however
it is not the case today.

E.