Ssreflect Users Discussion List

[Christian Doczkal <>]

Hello,

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.

In Lesson 2 I cannot even execute the initial Require Import as I get:

> 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?

Best,
Christian


[1] https://github.com/math-comp/wiki/wiki/tutorial-itp2016