Suppress erasable warning for props. #114
gebnerci.yml
on: push
build
/
build
22m 23s
nix
/
fstar-nix
20m 11s
stale-hints
/
check_stale_hints
9s
Matrix: tests / binary-smoke
Matrix: tests / ocaml-smoke
tests
/
check-stage3
6m 14s
tests
/
test-local
16m 9s
tests
/
perf-canaries
16s
ciok
0s
Annotations
3 errors, 6 warnings, and 7 notices
|
tests / test-local
Diff failed for files /tests/error-messages/_output/Monoid.fst.json_output and /tests/error-messages/Monoid.fst.json_output.expected:
--- _output/Monoid.fst.json_output 2025-01-10 22:37:21.400814821 +0000
+++ Monoid.fst.json_output.expected 2025-01-10 22:34:35.355480267 +0000
@@ -345,8 +345,8 @@
Module after type checking:
module Monoid
Declarations: [
-let right_unitality_lemma m u466 mult = forall (x: m). mult x u466 == x
-let left_unitality_lemma m u466 mult = forall (x: m). mult u466 x == x
+let right_unitality_lemma m u476 mult = forall (x: m). mult x u476 == x
+let left_unitality_lemma m u476 mult = forall (x: m). mult u476 x == x
let associativity_lemma m mult = forall (x: m) (y: m) (z: m). mult (mult x y) z == mult x (mult y z)
unopteq
type monoid (m: Type) =
@@ -382,25 +382,25 @@
-let intro_monoid m u466 mult = Monoid.Monoid u466 mult () () () <: Prims.Pure (Monoid.monoid m)
+let intro_monoid m u476 mult = Monoid.Monoid u476 mult () () () <: Prims.Pure (Monoid.monoid m)
let nat_plus_monoid =
let add x y = x + y <: Prims.nat in
Monoid.intro_monoid Prims.nat 0 add
let int_plus_monoid = Monoid.intro_monoid Prims.int 0 Prims.op_Addition
let conjunction_monoid =
- let u464 = FStar.Pervasives.singleton Prims.l_True in
+ let u474 = FStar.Pervasives.singleton Prims.l_True in
let mult p q = p /\ q <: Prims.prop in
let left_unitality_helper p =
- (assert (mult u464 p <==> p);
- FStar.PropositionalExtensionality.apply (mult u464 p) p)
+ (assert (mult u474 p <==> p);
+ FStar.PropositionalExtensionality.apply (mult u474 p) p)
<:
- FStar.Pervasives.Lemma (ensures mult u464 p == p)
+ FStar.Pervasives.Lemma (ensures mult u474 p == p)
in
let right_unitality_helper p =
- (assert (mult p u464 <==> p);
- FStar.PropositionalExtensionality.apply (mult p u464) p)
+ (assert (mult p u474 <==> p);
+ FStar.PropositionalExtensionality.apply (mult p u474) p)
<:
- FStar.Pervasives.Lemma (ensures mult p u464 == p)
+ FStar.Pervasives.Lemma (ensures mult p u474 == p)
in
let associativity_helper p1 p2 p3 =
(assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3));
@@ -409,26 +409,26 @@
FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3))
in
FStar.Classical.forall_intro right_unitality_helper;
- assert (Monoid.right_unitality_lemma Prims.prop u464 mult);
+ assert (Monoid.right_unitality_lemma Prims.prop u474 mult);
FStar.Classical.forall_intro left_unitality_helper;
- assert (Monoid.left_unitality_lemma Prims.prop u464 mult);
+ assert (Monoid.left_unitality_lemma Prims.prop u474 mult);
FStar.Classical.forall_intro_3 associativity_helper;
assert (Monoid.associativity_lemma Prims.prop mult);
- Monoid.intro_monoid Prims.prop u464 mult
+ Monoid.intro_monoid Prims.prop u474 mult
let disjunction_monoid =
- let u464 = FStar.Pervasives.singleton Prims.l_False in
+ let u474 = FStar.Pervasives.singleton Prims.l_False in
let mult p q = p \/ q <: Prims.prop in
let left_unitality_helper p =
- (assert (mult u464 p <==> p);
- FStar.PropositionalExtensionality.apply (mult u464 p) p)
+ (assert (mult u474 p <==> p);
+ FStar.PropositionalExtensionality.apply (mult u474 p) p)
<:
- FStar.Pervasives.Lemma (ensures mult u464 p == p)
+ FStar.Pervasives.Lemma (ensures mult u474 p == p)
in
let right_unitality_helper p =
- (assert (mult p u464 <==> p);
- FStar.PropositionalExtensionality.apply (mult p u464) p)
+ (assert (mult p u474 <==> p);
+ FStar.PropositionalExtensionality.apply (mult p u474) p)
<:
- FStar.Pervasives.Lemma (ensures mult p u464 == p)
+ FStar.Pervasives.Lemma (ensures mult p u474 == p)
in
let associativity_helper p1 p2 p3 =
(assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3));
@@ -437,12 +437,12 @@
FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3))
in
FStar.Classical.forall_intro right_unitality_helper;
- assert (Monoid.right_unitality_lemma Prims.prop u464 mult);
+ assert (Monoid.rig
|
|
tests / test-local
Diff failed for files /tests/error-messages/_output/Monoid.fst.output and /tests/error-messages/Monoid.fst.output.expected:
--- _output/Monoid.fst.output 2025-01-10 22:37:22.408822988 +0000
+++ Monoid.fst.output.expected 2025-01-10 22:34:35.355480267 +0000
@@ -345,8 +345,8 @@
Module after type checking:
module Monoid
Declarations: [
-let right_unitality_lemma m u466 mult = forall (x: m). mult x u466 == x
-let left_unitality_lemma m u466 mult = forall (x: m). mult u466 x == x
+let right_unitality_lemma m u476 mult = forall (x: m). mult x u476 == x
+let left_unitality_lemma m u476 mult = forall (x: m). mult u476 x == x
let associativity_lemma m mult = forall (x: m) (y: m) (z: m). mult (mult x y) z == mult x (mult y z)
unopteq
type monoid (m: Type) =
@@ -382,25 +382,25 @@
-let intro_monoid m u466 mult = Monoid.Monoid u466 mult () () () <: Prims.Pure (Monoid.monoid m)
+let intro_monoid m u476 mult = Monoid.Monoid u476 mult () () () <: Prims.Pure (Monoid.monoid m)
let nat_plus_monoid =
let add x y = x + y <: Prims.nat in
Monoid.intro_monoid Prims.nat 0 add
let int_plus_monoid = Monoid.intro_monoid Prims.int 0 Prims.op_Addition
let conjunction_monoid =
- let u464 = FStar.Pervasives.singleton Prims.l_True in
+ let u474 = FStar.Pervasives.singleton Prims.l_True in
let mult p q = p /\ q <: Prims.prop in
let left_unitality_helper p =
- (assert (mult u464 p <==> p);
- FStar.PropositionalExtensionality.apply (mult u464 p) p)
+ (assert (mult u474 p <==> p);
+ FStar.PropositionalExtensionality.apply (mult u474 p) p)
<:
- FStar.Pervasives.Lemma (ensures mult u464 p == p)
+ FStar.Pervasives.Lemma (ensures mult u474 p == p)
in
let right_unitality_helper p =
- (assert (mult p u464 <==> p);
- FStar.PropositionalExtensionality.apply (mult p u464) p)
+ (assert (mult p u474 <==> p);
+ FStar.PropositionalExtensionality.apply (mult p u474) p)
<:
- FStar.Pervasives.Lemma (ensures mult p u464 == p)
+ FStar.Pervasives.Lemma (ensures mult p u474 == p)
in
let associativity_helper p1 p2 p3 =
(assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3));
@@ -409,26 +409,26 @@
FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3))
in
FStar.Classical.forall_intro right_unitality_helper;
- assert (Monoid.right_unitality_lemma Prims.prop u464 mult);
+ assert (Monoid.right_unitality_lemma Prims.prop u474 mult);
FStar.Classical.forall_intro left_unitality_helper;
- assert (Monoid.left_unitality_lemma Prims.prop u464 mult);
+ assert (Monoid.left_unitality_lemma Prims.prop u474 mult);
FStar.Classical.forall_intro_3 associativity_helper;
assert (Monoid.associativity_lemma Prims.prop mult);
- Monoid.intro_monoid Prims.prop u464 mult
+ Monoid.intro_monoid Prims.prop u474 mult
let disjunction_monoid =
- let u464 = FStar.Pervasives.singleton Prims.l_False in
+ let u474 = FStar.Pervasives.singleton Prims.l_False in
let mult p q = p \/ q <: Prims.prop in
let left_unitality_helper p =
- (assert (mult u464 p <==> p);
- FStar.PropositionalExtensionality.apply (mult u464 p) p)
+ (assert (mult u474 p <==> p);
+ FStar.PropositionalExtensionality.apply (mult u474 p) p)
<:
- FStar.Pervasives.Lemma (ensures mult u464 p == p)
+ FStar.Pervasives.Lemma (ensures mult u474 p == p)
in
let right_unitality_helper p =
- (assert (mult p u464 <==> p);
- FStar.PropositionalExtensionality.apply (mult p u464) p)
+ (assert (mult p u474 <==> p);
+ FStar.PropositionalExtensionality.apply (mult p u474) p)
<:
- FStar.Pervasives.Lemma (ensures mult p u464 == p)
+ FStar.Pervasives.Lemma (ensures mult p u474 == p)
in
let associativity_helper p1 p2 p3 =
(assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3));
@@ -437,12 +437,12 @@
FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3))
in
FStar.Classical.forall_intro right_unitality_helper;
- assert (Monoid.right_unitality_lemma Prims.prop u464 mult);
+ assert (Monoid.right_unitality_lemma P
|
|
tests / test-local
Process completed with exit code 2.
|
|
stale-hints / check_stale_hints
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
nix / fstar-nix
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
build / build
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
tests / check-stage3
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-latest)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
tests / test-local
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
tests / perf-canaries:
DEFS_100#L1
time = 0.15
|
|
tests / perf-canaries:
DEFS_200#L1
time = 0.17
|
|
tests / perf-canaries:
DEFS_400#L1
time = 0.18
|
|
tests / perf-canaries:
DEFS_800#L1
time = 0.22
|
|
tests / perf-canaries:
DEFS_1600#L1
time = 0.32
|
|
tests / perf-canaries:
DEFS_3200#L1
time = 0.49
|
|
tests / perf-canaries:
DEFS_6400#L1
time = 0.85
|
Artifacts
Produced during runtime
| Name | Size | |
|---|---|---|
|
fstar-repo
|
311 MB |
|
|
fstar-src.tar.gz
|
4.98 MB |
|
|
fstar.tar.gz
|
137 MB |
|