Skip to content

rust: use doc comments #715

rust: use doc comments

rust: use doc comments #715

Re-run triggered September 26, 2023 18:11
Status Success
Total duration 7h 36m 27s
Artifacts 2

docker-coq.yml

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

Annotations

5 errors and 23 warnings
master
Makefile.coq:847: src/Coqprime/Tactic/Tactic.v
master
Makefile.coq.noex:847: /github/workspace/rupicola/bedrock2/bedrock2/src/bedrock2/MetricLogging.v
master
Makefile.coq.noex:417: all
master
Makefile:42: noex
master
Makefile:102: bedrock2_noex
master
Non-empty-diff: diff --git a/fiat-rust/src/curve25519_32.rs b/fiat-rust/src/curve25519_32.rs index 13c4f90..88239dc 100644 --- a/fiat-rust/src/curve25519_32.rs +++ b/fiat-rust/src/curve25519_32.rs @@ -20,8 +20,8 @@ pub type fiat_25519_i1 = i8; pub type fiat_25519_u2 = u8; pub type fiat_25519_i2 = i8; -/* The type fiat_25519_loose_field_element is a field element with loose bounds. */ -/* Bounds: [[0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000]] */ +/** The type fiat_25519_loose_field_element is a field element with loose bounds. */ +/** Bounds: [[0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000]] */ #[derive(Clone, Copy)] pub struct fiat_25519_loose_field_element(pub [u32; 10]); @@ -40,8 +40,8 @@ impl core::ops::IndexMut<usize> for fiat_25519_loose_field_element { } } -/* The type fiat_25519_tight_field_element is a field element with tight bounds. */ -/* Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000]] */ +/** The type fiat_25519_tight_field_element is a field element with tight bounds. */ +/** Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000]] */ #[derive(Clone, Copy)] pub struct fiat_25519_tight_field_element(pub [u32; 10]); diff --git a/fiat-rust/src/curve25519_64.rs b/fiat-rust/src/curve25519_64.rs index 9796032..4622b7f 100644 --- a/fiat-rust/src/curve25519_64.rs +++ b/fiat-rust/src/curve25519_64.rs @@ -20,8 +20,8 @@ pub type fiat_25519_i1 = i8; pub type fiat_25519_u2 = u8; pub type fiat_25519_i2 = i8; -/* The type fiat_25519_loose_field_element is a field element with loose bounds. */ -/* Bounds: [[0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]] */ +/** The type fiat_25519_loose_field_element is a field element with loose bounds. */ +/** Bounds: [[0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]] */ #[derive(Clone, Copy)] pub struct fiat_25519_loose_field_element(pub [u64; 5]); @@ -40,8 +40,8 @@ impl core::ops::IndexMut<usize> for fiat_25519_loose_field_element { } } -/* The type fiat_25519_tight_field_element is a field element with tight bounds. */ -/* Bounds: [[0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]] */ +/** The type fiat_25519_tight_field_element is a field element with tight bounds. */ +/** Bounds: [[0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]] */ #[derive(Clone, Copy)] pub struct fiat_25519_tight_field_element(pub [u64; 5]); diff --git a/fiat-rust/src/curve25519_scalar_32.rs b/fiat-rust/src/curve25519_scalar_32.rs index 23d65a5..368b481 100644 --- a/fiat-rust/src/curve25519_scalar_32.rs +++ b/fiat-rust/src/curve25519_scalar_32.rs @@ -25,8 +25,8 @@ pub type fiat_25519_scalar_i1 = i8; pub type fiat_25519_scalar_u2 = u8; pub type fiat_25519_scalar_i2 = i8; -/* The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ -/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ +/** The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ +/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffff
master
Could not find a terminator for warning: File "./src/Rewriter/Util/NatUtil.v", line 53, 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/Rewriter/Util/NatUtil.v", line 54, 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 71, 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/Rewriter/Util/NatUtil.v", line 71, 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/Rewriter/Util/NatUtil.v", line 73, 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/Rewriter/Util/NatUtil.v", line 73, 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/Rewriter/Util/NatUtil.v", line 87, 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/Rewriter/Util/NatUtil.v", line 86, 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/Rewriter/Util/NatUtil.v", line 193, 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 193, 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
Non-empty-diff: diff --git a/fiat-rust/src/curve25519_32.rs b/fiat-rust/src/curve25519_32.rs index 13c4f90..88239dc 100644 --- a/fiat-rust/src/curve25519_32.rs +++ b/fiat-rust/src/curve25519_32.rs @@ -20,8 +20,8 @@ pub type fiat_25519_i1 = i8; pub type fiat_25519_u2 = u8; pub type fiat_25519_i2 = i8; -/* The type fiat_25519_loose_field_element is a field element with loose bounds. */ -/* Bounds: [[0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000]] */ +/** The type fiat_25519_loose_field_element is a field element with loose bounds. */ +/** Bounds: [[0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000]] */ #[derive(Clone, Copy)] pub struct fiat_25519_loose_field_element(pub [u32; 10]); @@ -40,8 +40,8 @@ impl core::ops::IndexMut<usize> for fiat_25519_loose_field_element { } } -/* The type fiat_25519_tight_field_element is a field element with tight bounds. */ -/* Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000]] */ +/** The type fiat_25519_tight_field_element is a field element with tight bounds. */ +/** Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000]] */ #[derive(Clone, Copy)] pub struct fiat_25519_tight_field_element(pub [u32; 10]); diff --git a/fiat-rust/src/curve25519_64.rs b/fiat-rust/src/curve25519_64.rs index 9796032..4622b7f 100644 --- a/fiat-rust/src/curve25519_64.rs +++ b/fiat-rust/src/curve25519_64.rs @@ -20,8 +20,8 @@ pub type fiat_25519_i1 = i8; pub type fiat_25519_u2 = u8; pub type fiat_25519_i2 = i8; -/* The type fiat_25519_loose_field_element is a field element with loose bounds. */ -/* Bounds: [[0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]] */ +/** The type fiat_25519_loose_field_element is a field element with loose bounds. */ +/** Bounds: [[0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]] */ #[derive(Clone, Copy)] pub struct fiat_25519_loose_field_element(pub [u64; 5]); @@ -40,8 +40,8 @@ impl core::ops::IndexMut<usize> for fiat_25519_loose_field_element { } } -/* The type fiat_25519_tight_field_element is a field element with tight bounds. */ -/* Bounds: [[0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]] */ +/** The type fiat_25519_tight_field_element is a field element with tight bounds. */ +/** Bounds: [[0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]] */ #[derive(Clone, Copy)] pub struct fiat_25519_tight_field_element(pub [u64; 5]); diff --git a/fiat-rust/src/curve25519_scalar_32.rs b/fiat-rust/src/curve25519_scalar_32.rs index 23d65a5..368b481 100644 --- a/fiat-rust/src/curve25519_scalar_32.rs +++ b/fiat-rust/src/curve25519_scalar_32.rs @@ -25,8 +25,8 @@ pub type fiat_25519_scalar_i1 = i8; pub type fiat_25519_scalar_u2 = u8; pub type fiat_25519_scalar_i2 = i8; -/* The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ -/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ +/** The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ +/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffff
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 431d7a6 nothing to commit, working tree clean Entering 'etc/coq-scripts' HEAD detached at 8b66ebe nothing to commit, working tree clean Entering 'rewriter' HEAD detached at 26f5c84 nothing to commit, working tree clean Entering 'rewriter/etc/coq-scripts' HEAD detached at 8ce1d5d nothing to commit, working tree clean Entering 'rupicola' HEAD detached at 6d4f40c nothing to commit, working tree clean Entering 'rupicola/bedrock2' HEAD detached at b36804f 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 1b632be 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