Github actions CI #4
ci.yml
on: pull_request
build-and-test
20m 53s
Matrix: build-krmllib
publish_book
0s
ciok
0s
Annotations
22 warnings
build-and-test
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
build-and-test:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/karamel/karamel/FStar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
build-and-test:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/karamel/karamel/FStar/ulib/FStar.UInt.fst(293,8-293,25):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
- See also /__w/karamel/karamel/FStar/ulib/FStar.UInt.fsti(435,8-435,51)
|
build-and-test:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/karamel/karamel/FStar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
build-and-test:
FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti#L446
(288) * Warning 288 at /__w/karamel/karamel/FStar/ulib/FStar.Reflection.V2.Arith.fst(116,20-116,31):
- FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated
- Use Reflection.term_eq instead
- See also /__w/karamel/karamel/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(446,0-446,42)
|
build-and-test:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/karamel/karamel/FStar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
build-and-test:
FStar/src/data/FStarC.Compiler.RBSet.fst#L105
(337) * Warning 337 at /__w/karamel/karamel/FStar/src/data/FStarC.Compiler.RBSet.fst(105,30-105,31):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
build-and-test:
FStar/src/data/FStarC.Compiler.RBSet.fst#L105
(337) * Warning 337 at /__w/karamel/karamel/FStar/src/data/FStarC.Compiler.RBSet.fst(105,36-105,37):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
build-and-test:
FStar/src/basic/FStarC.Compiler.Plugins.fst#L86
(337) * Warning 337 at /__w/karamel/karamel/FStar/src/basic/FStarC.Compiler.Plugins.fst(86,16-86,17):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
build-and-test:
FStar/src/basic/FStarC.Compiler.Plugins.fst#L87
(337) * Warning 337 at /__w/karamel/karamel/FStar/src/basic/FStarC.Compiler.Plugins.fst(87,16-87,17):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
build-and-test:
FStar/src/basic/FStarC.Compiler.Plugins.fst#L88
(337) * Warning 337 at /__w/karamel/karamel/FStar/src/basic/FStarC.Compiler.Plugins.fst(88,16-88,17):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
build-and-test:
Spec.Loops.fst#L47
(328) * Warning 328 at Spec.Loops.fst(47,8-47,19):
- Global binding
'Spec.Loops.repeat_base'
is recursive but not used in its body
|
build-and-test:
FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(45,13-45,20):
- FStar.Krml.Endianness.le_to_n is deprecated
- FStar.Endianness.le_to_n
- See also FStar.Krml.Endianness.fst(21,8-21,15)
|
build-and-test:
FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(47,8-47,32):
- FStar.Krml.Endianness.le_to_n is deprecated
- FStar.Endianness.le_to_n
- See also FStar.Krml.Endianness.fst(21,8-21,15)
|
build-and-test:
FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(55,11-55,18):
- FStar.Krml.Endianness.le_to_n is deprecated
- FStar.Endianness.le_to_n
- See also FStar.Krml.Endianness.fst(21,8-21,15)
|
build-and-test:
FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(56,11-56,18):
- FStar.Krml.Endianness.le_to_n is deprecated
- FStar.Endianness.le_to_n
- See also FStar.Krml.Endianness.fst(21,8-21,15)
|
build-and-test:
FStar.Krml.Endianness.fst#L36
(288) * Warning 288 at FStar.Krml.Endianness.fst(57,4-57,28):
- FStar.Krml.Endianness.lemma_euclidean_division is deprecated
- FStar.Endianness.lemma_euclidean_division
- See also FStar.Krml.Endianness.fst(36,4-36,28)
|
build-and-test:
FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(57,56-57,63):
- FStar.Krml.Endianness.le_to_n is deprecated
- FStar.Endianness.le_to_n
- See also FStar.Krml.Endianness.fst(21,8-21,15)
|
build-and-test:
FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(58,11-58,18):
- FStar.Krml.Endianness.le_to_n is deprecated
- FStar.Endianness.le_to_n
- See also FStar.Krml.Endianness.fst(21,8-21,15)
|
build-and-test:
FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(58,34-58,41):
- FStar.Krml.Endianness.le_to_n is deprecated
- FStar.Endianness.le_to_n
- See also FStar.Krml.Endianness.fst(21,8-21,15)
|
build-and-test:
FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(59,11-59,18):
- FStar.Krml.Endianness.le_to_n is deprecated
- FStar.Endianness.le_to_n
- See also FStar.Krml.Endianness.fst(21,8-21,15)
|
ciok
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
Artifacts
Produced during runtime
Name | Size | |
---|---|---|
book
|
3.27 MB |
|