search

GeoCoq / GeoCoq

A formalization of geometry in Coq based on Tarski's axiom system
GNU Lesser General Public License v3.0
184 stars 26 forks source link

today i install again in new virtual machine have make error #4

Closed hoyeunglee closed 8 years ago

hoyeunglee commented 8 years ago

rojection "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/par_perp_2_par_par_perp_perp "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/par_perp_perp_TCP "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/par_perp_perp_par_perp_2_par "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/par_perp_perp_playfair "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/par_trans_playfair "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/par_trans_proclus "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/playfair_alternate_interior_angles "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/playfair_bis_playfair "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/playfair_par_trans_par_perp_perp

Killed make: * [Meta_theory/Parallel_postulates/playfair_par_trans_par_perp_perp.vo] Error 137 martin@ubuntu:~/hilbertreborn/GeoCoq$ martin@ubuntu:~/hilbertreborn/GeoCoq$ martin@ubuntu:~/hilbertreborn/GeoCoq$ make "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/playfair_par_trans_par_perp_perp Killed make: * [Meta_theory/Parallel_postulates/playfair_par_trans_par_perp_perp.vo] Error 137 martin@ubuntu:~/hilbertreborn/GeoCoq$ coqc -v The Coq Proof Assistant, version 8.4pl6 (December 2015) compiled on Dec 17 2015 02:29:20 with OCaml 3.12.1 martin@ubuntu:~/hilbertreborn/GeoCoq$ lsb_release -a No LSB modules are available. Distributor ID: Ubuntu Description: Ubuntu 12.04.5 LTS Release: 12.04 Codename: precise martin@ubuntu:~/hilbertreborn/GeoCoq$

hoyeunglee commented 8 years ago

in new ubuntu 14.04 also got error

"coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/par_perp_perp_playfair "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/par_trans_playfair "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/par_trans_proclus "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/playfair_alternate_interior_angles "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/playfair_bis_playfair "coqc" -q -R . GeoCoq Meta_theory/Parallel_postulates/playfair_par_trans_par_perp_perp Killed make: *\ [Meta_theory/Parallel_postulates/playfair_par_trans_par_perp_perp.vo] Error 137 martin@ubuntu:~/hilbertreborn/GeoCoq$ make

jnarboux commented 8 years ago

It is problably a out of memory error code. You should increase the memory of your VM.

Julien