separate partitioned facts

17 jobs for partitioned in 8 minutes and 40 seconds (queued for 6 seconds)
Status Job ID Name Coverage
  Build
passed #83808
1.10.0-coq-8.10

00:08:39

passed #83809
1.10.0-coq-8.11

00:08:39

failed #83807
1.10.0-coq-8.9

00:03:27

passed #83805
1.9.0-coq-8.10

00:08:37

passed #83806
1.9.0-coq-8.11

00:05:24

failed #83804
1.9.0-coq-8.9

00:03:47

passed #83810
build-for-process

00:02:34

passed #83811
build-for-process-classic

00:03:33

failed #83814
allowed to fail
coq-8.10

00:03:13

failed #83815
allowed to fail
coq-dev

00:06:27

passed #83812
proof-length

00:00:56

failed #83813
spell-check

00:00:56

 
  Process
passed #83818
doc

00:00:51

passed #83819
doc-classic

00:01:09

passed #83820
proof-state

00:05:44

passed #83816
validate

00:01:48

passed #83817
validate-classic

00:02:17

 
Name Stage Failure
failed
coq-dev Build
# Warning: omega is deprecated since 8.12; use “lia” instead.
# [omega-is-deprecated,deprecated]
# File "./classic/analysis/uni/basic/tdma_wcrt_analysis.v", line 811, characters 90-126:
# Warning: omega is deprecated since 8.12; use “lia” instead.
# [omega-is-deprecated,deprecated]
# make: *** [Makefile:343: all] Error 2

'opam install -y -v -j 2 coq-prosa' failed.
ERROR: Job failed: exit code 1
failed
1.9.0-coq-8.9 Build
- make: *** [Makefile:327: all] Error 2


<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-prosa dev
+-
- No changes have been performed
ERROR: Job failed: exit code 1
failed
1.10.0-coq-8.9 Build
#     (\big[_/_]_(i in _) _)
# does not match any subterm of the goal
#
# make[1]: *** [Makefile:679: analysis/facts/model/service_of_jobs.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make: *** [Makefile:327: all] Error 2

'opam install -y -v -j 2 coq-prosa' failed.
ERROR: Job failed: exit code 1
failed
coq-8.10 Build
# File "./classic/model/schedule/uni/susp/build_suspension_table.v", line 229, characters 20-85:
# Error: Unknown interpretation for notation "@ arg_maxP".
#
# make[1]: *** [Makefile:676: classic/model/schedule/uni/susp/build_suspension_table.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make: *** [Makefile:321: all] Error 2

'opam install -y -v -j 2 coq-prosa' failed.
ERROR: Job failed: exit code 1
failed
spell-check Build
Checking out 9f1add6d as partitioned...

Skipping Git submodules setup
Executing "step_script" stage of the job script
$ scripts/flag-typos-in-comments.sh `find . -iname '*.v' ! -path './classic/*'`
./model/schedule/partitioned.v: potentially misspelled word 'PState'
./model/schedule/partitioned.v: potentially misspelled word 'assignement'
./analysis/facts/model/partitioned.v: potentially misspelled word 'assignement'
ERROR: Job failed: exit code 1