Skip to content

[CI] Add checkout to test-rust-check-all #761

[CI] Add checkout to test-rust-check-all

[CI] Add checkout to test-rust-check-all #761

Triggered via push October 26, 2023 16:38
Status Success
Total duration 7h 5m 27s
Artifacts 2

docker-coq.yml

on: push
Matrix: docker-build
Fit to window
Zoom out
Zoom in

Annotations

5 errors and 22 warnings
master
Makefile.coq:847: src/Coqprime/Tactic/Tactic.v
master
Makefile.coq.noex:847: /github/workspace/rupicola/bedrock2/bedrock2/src/bedrock2/Lift1Prop.v
master
Makefile.coq.noex:417: all
master
Makefile:42: noex
master
Makefile:102: bedrock2_noex
master
Could not find a terminator for warning: File "./src/Rewriter/Util/NatUtil.v", line 53, characters 35-42: Warning: Notation mod_mod is deprecated since 8.17. Use Div0.mod_mod instead. [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Rewriter/Util/NatUtil.v", line 192, characters 43-50: Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead. [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Rewriter/Util/NatUtil.v", line 192, characters 43-50: Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead. [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Rewriter/Util/NatUtil.v", line 221, characters 12-23: Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead. [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Rewriter/Util/NatUtil.v", line 221, characters 12-23: Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead. [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Rewriter/Util/NatUtil.v", line 221, characters 12-23: Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead. [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Rewriter/Util/NatUtil.v", line 287, characters 28-36: Warning: Notation mod_same is deprecated since 8.17. Use Div0.mod_same instead. [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Rewriter/Util/NatUtil.v", line 287, characters 28-36: Warning: Notation mod_same is deprecated since 8.17. Use Div0.mod_same instead. [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Rewriter/Util/NatUtil.v", line 305, characters 10-17: Warning: Notation add_mod is deprecated since 8.17. Use Div0.add_mod instead. [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Rewriter/Util/NatUtil.v", line 305, characters 10-17: Warning: Notation add_mod is deprecated since 8.17. Use Div0.add_mod instead. [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
master
Non-empty-diff: diff --git a/rupicola b/rupicola --- a/rupicola +++ b/rupicola @@ -1 +1 @@ -Subproject commit e6daa5e6f08e20088caa550ebcb7a856711948d6 +Subproject commit e6daa5e6f08e20088caa550ebcb7a856711948d6-dirty Entering 'coqprime' Entering 'etc/coq-scripts' Entering 'rewriter' Entering 'rewriter/etc/coq-scripts' Entering 'rupicola' diff --git a/bedrock2 b/bedrock2 --- a/bedrock2 +++ b/bedrock2 @@ -1 +1 @@ -Subproject commit f5b29c5d7b174128a0de4c35e6b8813910d1c50e +Subproject commit f5b29c5d7b174128a0de4c35e6b8813910d1c50e-dirty Entering 'rupicola/bedrock2' diff --git a/deps/coq-record-update b/deps/coq-record-update --- a/deps/coq-record-update +++ b/deps/coq-record-update @@ -1 +1 @@ -Subproject commit 99280150f003159c7c6f955d415a7c28e91a13af +Subproject commit 99280150f003159c7c6f955d415a7c28e91a13af-dirty Entering 'rupicola/bedrock2/deps/coq-record-update' Entering 'rupicola/bedrock2/deps/coqutil' Entering 'rupicola/bedrock2/deps/coqutil/etc/coq-scripts' Entering 'rupicola/bedrock2/deps/kami' Entering 'rupicola/bedrock2/deps/riscv-coq' Entering 'coqprime' HEAD detached at d5935ca nothing to commit, working tree clean Entering 'etc/coq-scripts' HEAD detached at 2df5dbe nothing to commit, working tree clean Entering 'rewriter' HEAD detached at 2f9a755 nothing to commit, working tree clean Entering 'rewriter/etc/coq-scripts' HEAD detached at 2df5dbe nothing to commit, working tree clean Entering 'rupicola' HEAD detached at e6daa5e Changes not staged for commit: (use "git add <file>..." to update what will be committed) (use "git restore <file>..." to discard changes in working directory) (commit or discard the untracked or modified content in submodules) modified: bedrock2 (untracked content) no changes added to commit (use "git add" and/or "git commit -a") Entering 'rupicola/bedrock2' HEAD detached at f5b29c5 Changes not staged for commit: (use "git add <file>..." to update what will be committed) (use "git restore <file>..." to discard changes in working directory) (commit or discard the untracked or modified content in submodules) modified: deps/coq-record-update (untracked content) no changes added to commit (use "git add" and/or "git commit -a") Entering 'rupicola/bedrock2/deps/coq-record-update' HEAD detached at 9928015 Untracked files: (use "git add <file>..." to include in what will be committed) src/Lens.v.timing src/RecordSet.v.timing src/RecordUpdate.v.timing nothing added to commit but untracked files present (use "git add" to track) Entering 'rupicola/bedrock2/deps/coqutil' HEAD detached at 8b84b7a nothing to commit, working tree clean Entering 'rupicola/bedrock2/deps/coqutil/etc/coq-scripts' HEAD detached at 8b66ebe nothing to commit, working tree clean Entering 'rupicola/bedrock2/deps/kami' HEAD detached at a5f3efe nothing to commit, working tree clean Entering 'rupicola/bedrock2/deps/riscv-coq' HEAD detached at 3c623d8 nothing to commit, working tree clean ::remove-matcher owner=coq-problem-matcher::
master
Could not find a terminator for warning: File "./src/Util/NatUtil.v", line 14, characters 34-48: Warning: Notation plus_le_compat is deprecated since 8.16. The Arith.Plus file is obsolete. Use Nat.add_le_mono instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Util/NatUtil.v", line 16, characters 25-32: Warning: Notation mod_mod is deprecated since 8.17. Use Div0.mod_mod instead. [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Util/NatUtil.v", line 34, characters 13-32: Warning: Notation Min.min_case_strong is deprecated since 8.16. The Arith.Min file is obsolete. Use Nat.min_case_strong instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Util/NatUtil.v", line 34, characters 13-32: Warning: Notation Min.min_case_strong is deprecated since 8.16. The Arith.Min file is obsolete. Use Nat.min_case_strong instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Util/NatUtil.v", line 36, characters 13-32: Warning: Notation Max.max_case_strong is deprecated since 8.16. The Arith.Max file is obsolete. Use Nat.max_case_strong instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Util/NatUtil.v", line 36, characters 13-32: Warning: Notation Max.max_case_strong is deprecated since 8.16. The Arith.Max file is obsolete. Use Nat.max_case_strong instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Util/NatUtil.v", line 50, characters 44-63: Warning: Notation Max.max_case_strong is deprecated since 8.16. The Arith.Max file is obsolete. Use Nat.max_case_strong instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Util/NatUtil.v", line 49, characters 44-63: Warning: Notation Min.min_case_strong is deprecated since 8.16. The Arith.Min file is obsolete. Use Nat.min_case_strong instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Util/NatUtil.v", line 156, characters 43-50: Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead. [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
master
Could not find a terminator for warning: File "./src/Util/NatUtil.v", line 156, characters 43-50: Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead. [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
test-amd64
Non-empty-diff: diff --git a/src/ExtractionOCaml/base_conversion.v b/src/ExtractionOCaml/base_conversion.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/bedrock2_base_conversion.v b/src/ExtractionOCaml/bedrock2_base_conversion.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/bedrock2_dettman_multiplication.v b/src/ExtractionOCaml/bedrock2_dettman_multiplication.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/bedrock2_saturated_solinas.v b/src/ExtractionOCaml/bedrock2_saturated_solinas.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/bedrock2_solinas_reduction.v b/src/ExtractionOCaml/bedrock2_solinas_reduction.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/bedrock2_unsaturated_solinas.v b/src/ExtractionOCaml/bedrock2_unsaturated_solinas.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v b/src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/dettman_multiplication.v b/src/ExtractionOCaml/dettman_multiplication.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/perf_unsaturated_solinas.v b/src/ExtractionOCaml/perf_unsaturated_solinas.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/perf_word_by_word_montgomery.v b/src/ExtractionOCaml/perf_word_by_word_montgomery.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/saturated_solinas.v b/src/ExtractionOCaml/saturated_solinas.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/solinas_reduction.v b/src/ExtractionOCaml/solinas_reduction.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/unsaturated_solinas.v b/src/ExtractionOCaml/unsaturated_solinas.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/with_bedrock2_base_conversion.v b/src/ExtractionOCaml/with_bedrock2_base_conversion.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/with_bedrock2_dettman_multiplication.v b/src/ExtractionOCaml/with_bedrock2_dettman_multiplication.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/with_bedrock2_saturated_solinas.v b/src/ExtractionOCaml/with_bedrock2_saturated_solinas.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/with_bedrock2_solinas_reduction.v b/src/ExtractionOCaml/with_bedrock2_solinas_reduction.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v b/src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v b/src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v old mode 100644 new mode 100755 diff --git a/src/ExtractionOCaml/word_by_word_montgomery.v b/src/ExtractionOCaml/word_by_word_montgomery.v old mode 100644 new mode 100755 Entering 'coqprime' Entering 'etc/coq-scripts' Entering 'rewriter' Entering 'rewriter/etc/coq-scripts' Entering 'rupicola' Entering 'rupicola/bedrock2' Entering 'rupicola/bedrock2/deps/coq-record-update' Entering 'rupicola/bedrock2/deps/coqutil' Entering 'rupicola/bedrock2/deps/coqutil/etc/coq-scripts' Entering 'rupicola/bedrock2/deps/kami' Entering 'rupicola/bedrock2/deps/riscv-coq' Entering 'coqprime' HEAD detached at d5935ca nothing to commit, working tree clean Entering 'etc/coq-scripts' HEAD detached at 2df5dbe nothing to commit, working tree clean Entering 'rewriter' HEAD detached at 2f9a755 nothing to commit, working tree clean Entering 'rewriter/etc/coq-scripts' HEAD detached at 2df5dbe nothing to commit, working tree clean Entering 'rupicola' HEAD detached at e6daa5e nothing to commit, working tree clean Entering 'rupicola/bedrock2' HEAD detached at f5b29c5 nothing to commit, working tree clean Entering 'rupicola/bedrock2/deps/coq-record-update' HEAD detached at 9928015 nothing to commit, working tree clean Entering 'rupicola/bedrock2/deps/coqutil' HEAD detached at 8b84b7a nothing to commit, working tree clean Entering 'rupicola/bedroc

Artifacts

Produced during runtime
Name Size
ExtractionHaskell-master Expired
1.77 GB
ExtractionOCaml-master Expired
3.11 GB