# 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>" "Charly Gries <Charly.Gries@etu.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.1.0.tar.gz" checksum: "md5=397b83bc884a6c07a005412e9a2e5b1f" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-geocoq.1.1.0 coq.8.4.5
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 8h opam install -y --deps-only coq-geocoq.1.1.0 coq.8.4.5
opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-geocoq.1.1.0 coq.8.4.5
Total: 30 M
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Coplanar_trans.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/ColR.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Utils/sets.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_prod.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_par_trans_par_perp_perp.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Highschool/triangle_midpoints_theorems.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch11_angles.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_sum.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_1.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Highschool/gravityCenter.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals_inter_dec.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_SPP_aux_3.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_lengths.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_SPP_aux_2.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Highschool/orientation.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_6_Desargues_Hessenberg.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_SPP_aux_1.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch08_orthogonality.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/Euclid.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_SPP_aux_4.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_5_Pappus_Pascal.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/project.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_tarski.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/vectors.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel_inter_dec.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/suma.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/TCP_tarski.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Axioms/hilbert_axioms.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch09_plane.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_order.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_4_cos.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_hilbert.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Utils/arity.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Highschool/orthocenter.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_playfair_bis.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_SPP.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Highschool/circumcenter.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_euclid.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/midpoints_playfair.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_3_angles.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_proclus.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Highschool/Euler_line.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity_2D.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_beeson.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Highschool/varignon.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_bet_identity.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch07_midpoint.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_playfair.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/independent_tarski_to_tarski.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Decidability/equivalence_between_decidability_properties_of_basic_relations.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_coinc_theory_for_concyclic.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_2_length.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Axioms/metric_axioms.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_aristotle.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Highschool/exercises.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_postulate_triangle.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Highschool/concyclic.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/perp_bisect.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_playfair_bis.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Axioms/independent_tarski_axioms.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tactics_axioms.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Axioms/beeson_s_axioms.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Coplanar_perm.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/Euclid_def.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_playfair.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Highschool/midpoint_thales.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Highschool/triangles.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Axioms/tarski_axioms.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch06_out_lines.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/Tagged_predicates.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/aristotle_greenberg.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_s_euclid_remove_degenerated_cases.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR_for_col.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_TCP.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_coinc_theory_for_cop.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch03_bet.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_midpoints.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_ID.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_2_par_par_perp_perp.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_proclus.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_alternate_interior_angles.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_SPP.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_bis_playfair.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_playfair.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch05_bet_le.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_par_perp_2_par.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_col.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_playfair_bis.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Axioms/makarios_variant_axioms.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch02_cong.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_coinc_theory_for_col.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/Permutations.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_cong_bet.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_col_theory.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_makarios.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_segment_construction.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Utils/general_tactics.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Utils/aux.vo
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/GeoCoq/Utils/all_equiv.vo
opam remove -y coq-geocoq.1.1.0