Ssreflect Users Discussion List

[Michael Nahas <>]

Hi Cristian,

For Coq, you can take a look at my tutorial:

   https://github.com/coq/www/blob/master/files/nahas_tutorial.v

It is just for Coq, not Ssreflect nor MathComp.  It a Coq file, not a PDF,  so people can install CoqIDE and walk through the file.  They will see not only what Coq looks like, but what the environment tells you.  It is very low-level and goes basic-step by basic-step with real examples.

A pretty-printed HTML version is here:

   https://mdnahas.github.io/doc/nahas_tutorial.html

Good luck,

Mike

On Tue, Jul 18, 2017 at 4:45 AM, 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