Skip to content

GitLab

R
rt-proofs

RT bound for partitioned scheduling

17 jobs for partitioned in 7 minutes and 26 seconds (queued for 6 seconds)
latest
1ff8d683
1 related merge request: !101 WIP: Partitioned
Status Job ID Name Coverage
  Build
passed #84132
1.10.0-coq-8.10

00:07:25

passed #84133
1.10.0-coq-8.11

00:05:30

failed #84131
1.10.0-coq-8.9

00:02:20

passed #84129
1.9.0-coq-8.10

00:05:26

passed #84130
1.9.0-coq-8.11

00:07:26

failed #84128
1.9.0-coq-8.9

00:02:59

passed #84134
build-for-process

00:02:00

passed #84135
build-for-process-classic

00:05:17

failed #84138
allowed to fail
coq-8.10

00:05:19

failed #84139
allowed to fail
coq-dev

00:05:01

passed #84136
proof-length

00:00:57

failed #84137
spell-check

00:00:54

 
  Process
passed #84142
doc

00:00:42

passed #84143
doc-classic

00:00:50

passed #84144
proof-state

00:05:07

passed #84140
validate

00:03:48

passed #84141
validate-classic

00:01:12

 
Name Stage Failure
failed
coq-8.10 Build 
'opam install -y -v -j 2 coq-prosa' failed.


<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-prosa dev
+- 
- No changes have been performed
ERROR: Job failed: exit code 1
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 
#     (\big[_/_]_(i in _) _)
# does not match any subterm of the goal
# 
# make[1]: *** [Makefile:680: 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
1.10.0-coq-8.9 Build 

Skipping Git submodules setup
Executing "step_script" stage of the job script
$ opam update -y

<><> Updating package repositories ><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] Could not update repository "coq-released": OpamDownload.Download_fail(_, "Curl failed: \"/usr/bin/curl --write-out %{http_code}\\\\n --retry 3 --retry-delay 2 --user-agent opam/2.0.7 -L -o /tmp/opam-12-5a61c5/index.tar.gz.part https://coq.inria.fr/opam/released/index.tar.gz\" exited with code 7")
[ERROR] Could not update repository "default": OpamDownload.Download_fail(_, "Curl failed: \"/usr/bin/curl --write-out %{http_code}\\\\n --retry 3 --retry-delay 2 --user-agent opam/2.0.7 -L -o /tmp/opam-12-ccabea/index.tar.gz.part https://opam.ocaml.org/index.tar.gz\" exited with code 7")
ERROR: Job failed: exit code 1
failed
spell-check Build 
Removing without-proofs/

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