« Up

geocoq 1.0.1 56 m 0 s 🏆

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-num            base        Num library distributed with the OCaml compiler
base-ocamlbuild     base        OCamlbuild binary and libraries distributed with the OCaml compiler
base-threads        base
base-unix           base
camlp5              7.14        Preprocessor-pretty-printer of OCaml
conf-findutils      1           Virtual package relying on findutils
conf-perl           2           Virtual package relying on perl
coq                 8.4.5       Formal proof management system.
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.02.3      The OCaml compiler (virtual package)
ocaml-base-compiler 4.02.3      Official 4.02.3 release
ocaml-config        1           OCaml Switch Configuration
ocamlbuild          0           Build system distributed with the OCaml compiler since OCaml 3.10.0
# opam file:
opam-version: "2.0"
maintainer: "Julien Narboux <julien@narboux.fr>"
homepage: "http://geocoq.github.io/GeoCoq/"
bug-reports: "https://github.com/GeoCoq/GeoCoq/issues"
authors: ["Gabriel Braun <gabriel.braun@unistra.fr>" "Pierre Boutry <pierre.boutry@unistra.fr>" "Julien Narboux <narboux@unistra.fr>"]
license: "LGPL 3"
build: [
  ["./configure.sh"]
  [make "-j%{jobs}%"]
]
install: [make "install"]
depends: [
  "ocaml"
  "coq" {>= "8.4pl4" & < "8.5~"}
]
tags: [
  "logpath:GeoCoq"
]
synopsis: "A formalization of geometry in Coq based on Tarski's axiom system"
url {
  src: "https://github.com/GeoCoq/GeoCoq/archive/1.0.1.tar.gz"
  checksum: "md5=5e656c305b8fd6c2e19a133d899067bd"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-geocoq.1.0.1 coq.8.4.5
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 8h opam install -y --deps-only coq-geocoq.1.0.1 coq.8.4.5
Return code
0
Duration
1 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-geocoq.1.0.1 coq.8.4.5
Return code
0
Duration
56 m 0 s

Installation size

Total: 27 M

  • 2 M ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/sets.vo
  • 2 M ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/CoappR.vo
  • 2 M ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/ColR.vo
  • 1 M ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch14_prod.vo
  • 1 M ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Euclid_1.vo
  • 1 M ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Euclid_2.vo
  • 1013 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch11_angles.vo
  • 1004 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Coplanar_trans_1.vo
  • 887 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Coplanar_trans_4.vo
  • 837 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch13_1.vo
  • 809 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Coplanar_trans_3.vo
  • 784 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch14_sum.vo
  • 775 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/gravityCenter.vo
  • 767 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/triangle_midpoints_theorems.vo
  • 714 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Euclid_aux_1.vo
  • 699 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Euclid_aux_3.vo
  • 685 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/quadrilaterals_inter_dec.vo
  • 658 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Euclid_aux_2.vo
  • 593 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch13_6_Desargues_Hessenberg.vo
  • 573 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch15_lengths.vo
  • 573 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/orientation.vo
  • 526 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Euclid_aux_4.vo
  • 478 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch08_orthogonality.vo
  • 377 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch13_5_Pappus_Pascal.vo
  • 365 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Coplanar_trans_2.vo
  • 334 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/project.vo
  • 307 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/quadrilaterals.vo
  • 296 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/vectors.vo
  • 292 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch12_parallel_inter_dec.vo
  • 282 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/hilbert_axioms.vo
  • 242 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch09_plane.vo
  • 241 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch14_order.vo
  • 230 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch12_parallel.vo
  • 222 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch13_4_cos.vo
  • 216 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/tarski_to_hilbert.vo
  • 202 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/arity.vo
  • 191 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/orthocenter.vo
  • 177 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch10_line_reflexivity_2D.vo
  • 168 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/circumcenter.vo
  • 164 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch10_line_reflexivity.vo
  • 148 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch13_3_angles.vo
  • 143 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Euclid.vo
  • 125 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Euler_line.vo
  • 124 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/tarski_axioms.vo
  • 119 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/unit_tests.vo
  • 116 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/tarski_to_beeson.vo
  • 112 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/varignon.vo
  • 108 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/counter_model_bet_identity.vo
  • 91 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch07_midpoint.vo
  • 83 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Coplanar_trans.vo
  • 74 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch13_2_length.vo
  • 71 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch05_bet_le.vo
  • 67 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/exercises.vo
  • 64 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/perp_bisect.vo
  • 63 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/concyclic.vo
  • 61 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/tactics_axioms.vo
  • 60 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Coplanar_perm.vo
  • 59 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Euclid_aux.vo
  • 55 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/triangles.vo
  • 53 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Euclid_def.vo
  • 53 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/midpoint_thales.vo
  • 52 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tagged_predicates.vo
  • 51 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch06_out_lines.vo
  • 45 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/tarski_to_coapp_theory_for_cop.vo
  • 44 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch03_bet.vo
  • 32 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch04_col.vo
  • 31 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch02_cong.vo
  • 23 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/tarski_to_coapp_theory_for_col.vo
  • 20 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Permutations.vo
  • 17 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Ch04_cong_bet.vo
  • 15 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/tarski_to_col_theory.vo
  • 13 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/tarski_to_makarios.vo
  • 12 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/counter_model_segment_construction.vo
  • 11 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/general_tactics.vo
  • 11 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/aux.vo
  • 4 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/intuitionistic_tarski_axioms.vo

Uninstall 🧹

Command
opam remove -y coq-geocoq.1.0.1
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣