HoTT / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
http://coq.inria.fr/
GNU Lesser General Public License v2.1
27 stars 5 forks source link

Most recent version of trunk-polyproj will not build #109

Closed JasonGross closed 10 years ago

JasonGross commented 10 years ago
jgross@cagnode17:~/coq-trunk-polyproj$ make -j10 -k
make --warn-undefined-variable --no-builtin-rules -f Makefile.build BUILDGRAMMAR=1 grammar/grammar.cma grammar/q_constr.cmo
make[1]: Entering directory `/afs/csail.mit.edu/u/j/jgross/coq-trunk-polyproj'
OCAMLDEP  plugins/funind/glob_termops.ml
I/O error: Input/output error
make[1]: `grammar/grammar.cma' is up to date.
make[1]: `grammar/q_constr.cmo' is up to date.
make[1]: Leaving directory `/afs/csail.mit.edu/u/j/jgross/coq-trunk-polyproj'
make --warn-undefined-variable --no-builtin-rules -f Makefile.build
make[1]: Entering directory `/afs/csail.mit.edu/u/j/jgross/coq-trunk-polyproj'
OCAMLDEP  plugins/funind/glob_termops.ml
I/O error: Input/output error
CHECK revision
make[1]: *** No rule to make target `plugins/funind/glob_termops.ml.d', needed by `plugins/funind/glob_termops.cmo'.
make[1]: Target `world' not remade because of errors.
make[1]: Leaving directory `/afs/csail.mit.edu/u/j/jgross/coq-trunk-polyproj'
make: *** [submake] Error 2
make: Target `NOARG' not remade because of errors.

Or with VERBOSE=1:

jgross@cagnode17:~/coq-trunk-polyproj$ make -j10 -k VERBOSE=1
make --warn-undefined-variable --no-builtin-rules -f Makefile.build BUILDGRAMMAR=1 grammar/grammar.cma grammar/q_constr.cmo
make[1]: Entering directory `/afs/csail.mit.edu/u/j/jgross/coq-trunk-polyproj'
"ocamldep" -slash -ml-synonym .ml4 -I config -I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I interp
 -I toplevel -I parsing -I printing -I grammar -I intf -I tools -I tools/coqdoc -I plugins/omega -I plugins/romega -I plugins/micromeg
a -I plugins/quote -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I plugins/fourier -I plugins/cc -I plugins/funind -I p
lugins/firstorder -I plugins/Derive -I plugins/rtauto -I plugins/nsatz -I plugins/syntax -I plugins/decl_mode -I plugins/btauto -I ide
 -I ide/utils "plugins/funind/glob_termops.ml" > "plugins/funind/glob_termops.ml.d" || (RV=$?; rm -f "plugins/funind/glob_termops.ml.d
"; exit ${RV})
I/O error: Input/output error
make[1]: `grammar/grammar.cma' is up to date.
make[1]: `grammar/q_constr.cmo' is up to date.
make[1]: Leaving directory `/afs/csail.mit.edu/u/j/jgross/coq-trunk-polyproj'
make --warn-undefined-variable --no-builtin-rules -f Makefile.build
make[1]: Entering directory `/afs/csail.mit.edu/u/j/jgross/coq-trunk-polyproj'
"ocamldep" -slash -ml-synonym .ml4 -I config -I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I interp
 -I toplevel -I parsing -I printing -I grammar -I intf -I tools -I tools/coqdoc -I plugins/omega -I plugins/romega -I plugins/micromeg
a -I plugins/quote -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I plugins/fourier -I plugins/cc -I plugins/funind -I p
lugins/firstorder -I plugins/Derive -I plugins/rtauto -I plugins/nsatz -I plugins/syntax -I plugins/decl_mode -I plugins/btauto -I ide
 -I ide/utils "plugins/funind/glob_termops.ml" > "plugins/funind/glob_termops.ml.d" || (RV=$?; rm -f "plugins/funind/glob_termops.ml.d"; exit ${RV})
I/O error: Input/output error
make[1]: *** No rule to make target `plugins/funind/glob_termops.ml.d', needed by `plugins/funind/glob_termops.cmo'.
rm -f revision.new
set -e; \
        if test -x "`which git`"; then \
          LANG=C; export LANG; \
          GIT_BRANCH=$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \
          GIT_HOST=$(hostname); \
          GIT_PATH=$(pwd); \
          (echo "${GIT_HOST}:${GIT_PATH},${GIT_BRANCH}") > revision.new; \
          (echo "$(git log -1 --pretty='format:%H')") >> revision.new; \
        fi
set -e; \
        if test -e revision.new; then \
          if test -e revision; then \
            if test "`cat revision`" = "`cat revision.new`" ; then \
               rm -f revision.new; \
            else \
               mv -f revision.new revision; \
            fi; \
          else \
            mv -f revision.new revision; \
          fi \
        fi
make[1]: Target `world' not remade because of errors.
make[1]: Leaving directory `/afs/csail.mit.edu/u/j/jgross/coq-trunk-polyproj'
make: *** [submake] Error 2
make: Target `NOARG' not remade because of errors.
jgross@cagnode17:~/coq-trunk-polyproj$

This is with ./configure -local on Linux cagnode17 2.6.32-5-xen-amd64 #1 SMP Sun Sep 23 13:49:30 UTC 2012 x86_64 GNU/Linux.

JasonGross commented 10 years ago

Nevermind, this was a problem on my end; for whatever reason, even less plugins/funind/glob_termops.ml gave me a read error. rm -f plugins/funind/glob_termops.ml && git reset --hard fixed things. (I guess rm -f plugins/funind/glob_termops.ml && git checkout HEAD plugins/funind/glob_termops.ml should have, too.)