Skip to content

Fix missing call to mangle + incorrect argument to namespace #309

Fix missing call to mangle + incorrect argument to namespace

Fix missing call to mangle + incorrect argument to namespace #309

Triggered via push February 3, 2026 21:41
Status Success
Total duration 20m 20s
Artifacts 1

ci.yml

on: push
Matrix: build-krmllib
publish_book
publish_book
ciok
ciok
Fit to window
Zoom out
Zoom in

Annotations

10 warnings
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(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(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#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(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#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(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(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(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: 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

Artifacts

Produced during runtime
Name Size Digest
book
3.27 MB
sha256:fa0bb912a1ebf83cb4897dd737df7e1ff9863660aa6b70dde96ef9a6ab50d200