Ssreflect Users Discussion List

["Sergey, Ilya" <>]

Dear Christian,

For teaching the very basics of Ssreflect/MathComp, you might these lecture notes and the accompanying sources:

http://ilyasergey.net/pnp

Kind regards,

Ilya 

On 18 Jul 2017, at 10:45, Christian Doczkal <> wrote:

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