(2020-06-26 21:49:50 UTC)
# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-num base Num library distributed with the OCaml compiler base-threads base base-unix base camlp5 7.12 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils coq 8.5.3 Formal proof management system. num 0 The Num library for arbitrary-precision integer and rational arithmetic ocaml 4.05.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.05.0 Official 4.05.0 release ocaml-config 1 OCaml Switch Configuration # opam file: opam-version: "2.0" maintainer: "matej.kosik@inria.fr" homepage: "https://github.com/coq-contribs/area-method" license: "Proprietary" build: [make "-j%{jobs}%"] install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/AreaMethod"] depends: [ "ocaml" "coq" {>= "8.5" & < "8.6~"} ] tags: [ "keyword:geometry" "keyword:chou gao zhang area method" "keyword:decision procedure" "category:Mathematics/Geometry/AutomatedDeduction" "date:2004-2010" ] authors: [ "Julien Narboux <>" ] bug-reports: "https://github.com/coq-contribs/area-method/issues" dev-repo: "git+https://github.com/coq-contribs/area-method.git" synopsis: "The Chou, Gao and Zhang area method" description: """ This contribution is the implementation of the Chou, Gao and Zhang's area method decision procedure for euclidean plane geometry. This development contains a partial formalization of the book "Machine Proofs in Geometry, Automated Production of Readable Proofs for Geometry Theorems" by Chou, Gao and Zhang. The examples shown automatically (there are more than 100 examples) includes the Ceva, Desargues, Menelaus, Pascal, Centroïd, Pappus, Gauss line, Euler line, Napoleon theorems. Changelog 2.1 : remove some not needed assumptions in some elimination lemmas (2010) 2.0 : extension implementation to Euclidean geometry (2009-2010) 1.0 : first implementation for affine geometry (2004)""" flags: light-uninstall url { src: "https://github.com/coq-contribs/area-method/archive/v8.5.0.tar.gz" checksum: "md5=ba9772aa2056aa4bc9ccc051a9a76a7f" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-area-method.8.5.0 coq.8.5.3
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 2h opam install -y --deps-only coq-area-method.8.5.0 coq.8.5.3
opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-area-method.8.5.0 coq.8.5.3
Total: 9 M
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_6.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_2.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_3.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_interactive.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_4.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/pythagoras_difference_lemmas.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/py_elimination_lemmas.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/pythagoras_difference_lemmas.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/py_elimination_lemmas.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/freepoints.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_5.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_centroid.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/my_field_tac.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/basic_geometric_facts.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/basic_geometric_facts.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/freepoints.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_circumcenter.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/ratios_elimination_lemmas.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/advanced_parallel_lemmas.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/advanced_parallel_lemmas.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_1.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/ratios_elimination_lemmas.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/Rgeometry_tools.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/my_field_tac.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/constructed_points_elimination.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/parallel_lemmas.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_interactive.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/tests_elimination_tactics_ratios.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/bench_normalization_tactics.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/pythagoras_difference.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/area_elimination_lemmas.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_2.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/parallel_lemmas.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/free_points_elimination.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/construction_lemmas.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/tests_elimination_tactics_py.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/geometry_tools.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/euclidean_constructions.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/bench_normalization_tactics.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/area_method.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/field_variable_isolation_tactic.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/area_coords_constructions.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/geometry_tools_lemmas.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/area_coords_constructions.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/elimination_prepare.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/tests_elimination_tactics_areas.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/field.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/euclidean_constructions_2.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_6.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/pythagoras_difference.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/area_elimination_lemmas.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/Rgeometry_tools.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/field_general_properties.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/tests_elimination_tactics_ratios.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/py_elimination_lemmas.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/construction_lemmas.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/tests_elimination_tactics_areas.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/construction_lemmas_2.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/chou_gao_zhang_axioms.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/pythagoras_difference_lemmas.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/constructed_points_elimination.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/tests_elimination_tactics_py.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/area_coords_elimination.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/simplify_constructions.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/construction_tactics.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/basic_geometric_facts.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/geometry_tools_lemmas.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/euclidean_constructions.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_3.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/advanced_parallel_lemmas.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/ratios_elimination_lemmas.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/constructed_points_elimination.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/geometry_tools.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_5.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/area_method.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/Rgeometry_tools.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/freepoints.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/chou_gao_zhang_axioms.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/field_variable_isolation_tactic.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/construction_lemmas_2.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/my_field_tac.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/elimination_prepare.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_interactive.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_centroid.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/area_coords_elimination.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/field_general_properties.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/bench_normalization_tactics.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/parallel_lemmas.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_1.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/field.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/euclidean_constructions_2.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_circumcenter.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/area_method.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/pythagoras_difference.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/geometry_tools.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/area_elimination_lemmas.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/field_variable_isolation_tactic.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/elimination_prepare.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_2.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/geometry_tools_lemmas.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/free_points_elimination.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_6.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/tests_elimination_tactics_py.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/construction_lemmas.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_4.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/tests_elimination_tactics_areas.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/tests_elimination_tactics_ratios.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/free_points_elimination.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/area_coords_constructions.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/field.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/euclidean_constructions.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/field_general_properties.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/simplify_constructions.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/euclidean_constructions_2.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/general_tactics.vo
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/chou_gao_zhang_axioms.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/construction_lemmas_2.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_3.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_1.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_5.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/construction_tactics.glob
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_centroid.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/simplify_constructions.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/area_coords_elimination.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_circumcenter.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/general_tactics.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/construction_tactics.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/examples_4.v
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/AreaMethod/general_tactics.glob
opam remove -y coq-area-method.8.5.0