# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils conf-gmp 4 Virtual package relying on a GMP lib system installation coq 8.14.0 Formal proof management system dune 3.7.0 Fast, portable, and opinionated build system ocaml 4.07.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.07.1 Official release 4.07.1 ocaml-config 1 OCaml Switch Configuration ocaml-secondary-compiler 4.08.1-1 OCaml 4.08.1 Secondary Switch Compiler ocamlfind 1.9.1 A library manager for OCaml ocamlfind-secondary 1.9.1 Adds support for ocaml-secondary-compiler to ocamlfind zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers # opam file: opam-version: "2.0" synopsis: "A Coq library for time and date arithmetic according to the UTC standard with leap seconds" # One-line description description: """ FV Time is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds (which are part of the UTC standard but usually not implemented in commercial libraries). """ # Longer description, can span several lines homepage: "https://gitlab.com/formalv/formalv" dev-repo: "git+https://gitlab.com/formalv/formalv" bug-reports: "https://gitlab.com/formalv/formalv/-/issues" doc: "https://gitlab.com/formalv/formalv/-/jobs/3104990375/artifacts/file/public/index.html" maintainer: "Mireia González Bedmar <mireia.gbedmar@formalv.com>" tags: [ "keyword:time" "keyword:date" "keyword:timestamp" "keyword:coq formalization" "logpath:formalv" ] authors: [ "Ana de Almeida Borges" "Quim Casals Buñuel" "Juan Conejero Rodriguez" "Mireia González Bedmar" "Eduardo Hermo Reyes" ] license: "PolyForm Noncommercial License 1.0.0" # Make sure this is reflected by a LICENSE file in your sources depends: [ "coq" {>= "8.14" & < "8.16~"} "coq-mathcomp-algebra" {>= "1.12" & < "1.15~" } "coq-mathcomp-ssreflect" {>= "1.12" & < "1.15~" } "coq-formalv-prim63_mathcomp" {= version} "coq-formalv-check_range" {= version} ] build: [ [make "-C" "theories/time" "-j" "%{jobs}%"] ] install: [ [make "-C" "theories/time" "install"] ] url { src: "https://gitlab.com/formalv/formalv/-/archive/1.0.1/formalv-1.0.1.tar.gz" checksum: "sha256=d00453d3f553c988df1ea1fd3a33413af03a2e21952b75b0c47f9290ae31b3bc" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-formalv-time.1.0.1 coq.8.14.0
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-formalv-time.1.0.1 coq.8.14.0
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-formalv-time.1.0.1 coq.8.14.0
Total: 6 M
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/formalTimeR.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/Hinnant.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/fvtm_extraction_correct.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/HinnantR.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/Hinnant.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/calendar.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/fvtm_extraction_correct.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/HinnantR.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/calendar.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/formalTimeR.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/formalTime.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/formalTime.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/table.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/fvtm_extraction.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/table.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/fvtm_extraction.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/formalTimeR.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/fvtm_extraction_correct.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/HinnantR.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/calendar.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/Hinnant.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/formalTime.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/doe_of_yoeK.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/doe_of_yoeK.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/fvtm_extraction.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/all_time.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/table.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/doe_of_yoeK.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/all_time.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/formalv/time/all_time.glob
opam remove -y coq-formalv-time.1.0.1