CI: compile the tutorial with alectryon

16 jobs for !134 with tutorial in 10 minutes and 47 seconds (queued for 6 seconds)
detached
Status Job ID Name Coverage
  Build
passed 1.10.0-coq-8.11 #136407

00:04:32

passed 1.11.0-coq-8.11 #136408

00:04:30

passed 1.11.0-coq-8.12 #136409

00:03:53

passed 1.12.0-coq-8.13 #136410

00:03:25

passed compile #136411

00:01:08

passed compile-classic #136412

00:02:02

passed coq-8.13 #136415

00:03:07

failed coq-dev #136416
allowed to fail

00:00:41

passed proof-length #136413

00:00:06

passed proof-state #136418

00:06:16

failed spell-check #136414

00:00:13

passed tutorial #136417

00:01:04

 
  Process
passed doc #136421

00:00:15

passed doc-classic #136422

00:00:29

passed validate #136419

00:00:47

passed validate-classic #136420

00:01:07

 
Name Stage Failure
failed
coq-dev Build
# Use iotaD instead. [deprecated-syntactic-definition,deprecated]
# File "./util/nondecreasing.v", line 632, characters 27-35:
# Warning: Notation iota_add is deprecated since mathcomp 1.13.0.
# Use iotaD instead. [deprecated-syntactic-definition,deprecated]
# make: *** [Makefile:386: all] Error 2

'opam install -y -v -j 2 coq-prosa' failed.
Cleaning up file based variables
ERROR: Job failed: exit code 1
failed
spell-check Build
./doc/tutorial.v: potentially misspelled word 'priori'
./doc/tutorial.v: potentially misspelled word 'proog'
./doc/tutorial.v: potentially misspelled word 'py'
./doc/tutorial.v: potentially misspelled word 'rst'
./doc/tutorial.v: potentially misspelled word 'typeclasses'
./doc/tutorial.v: potentially misspelled word 'webpage'
./doc/tutorial.v: potentially misspelled word 'whcich'
Cleaning up file based variables
ERROR: Job failed: exit code 1