Skip to content
Permalink
Browse files

Strip -no-native-compiler

It's not needed in Coq >= 8.5rc1 (or 8.5beta3?)
  • Loading branch information
JasonGross committed Jan 23, 2016
1 parent 7d0a107 commit 88ed234763b450f2dcf9cf73c2d15205fc70c1f5
Showing with 11 additions and 11 deletions.
  1. +1 −1 Makefile.am
  2. +1 −1 coq/theories/.dir-locals.el
  3. +2 −2 etc/ci/install_coq.sh
  4. +1 −1 etc/dpdgraph-0.4alpha/hoqthmdep
  5. +1 −1 hoq-config.in
  6. +1 −1 hoqc
  7. +1 −1 hoqdep
  8. +1 −1 hoqide
  9. +1 −1 hoqtop
  10. +1 −1 hoqtop.byte
@@ -185,7 +185,7 @@ checkproofs:

$(STD_VOFILES) : %.vo : %.v coq-HoTT
$(VECHO) COQTOP $*
$(Q) $(TIMER) etc/pipe_out.sh "$*.timing" "$(COQTOP)" -time -indices-matter -boot -nois -no-native-compiler -coqlib "$(SRCCOQLIB)" -R "$(SRCCOQLIB)/theories" Coq -compile "$*"
$(Q) $(TIMER) etc/pipe_out.sh "$*.timing" "$(COQTOP)" -time -indices-matter -boot -nois -coqlib "$(SRCCOQLIB)" -R "$(SRCCOQLIB)/theories" Coq -compile "$*"


# The HoTT library as a single target
@@ -1,4 +1,4 @@
((coq-mode . ((eval . (let ((default-directory (locate-dominating-file
buffer-file-name ".dir-locals.el")))
(make-local-variable 'coq-prog-args)
(setq coq-prog-args `("-no-native-compiler" "-indices-matter" "-boot" "-nois" "-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq" "-emacs")))))))
(setq coq-prog-args `("-indices-matter" "-boot" "-nois" "-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq" "-emacs")))))))
@@ -37,8 +37,8 @@ if [ ! -z "$FORCE_COQ_VERSION" ]
then
git checkout "$FORCE_COQ_VERSION" || exit $?
fi
echo '$ ./configure -no-native-compiler '"$@"
./configure -no-native-compiler "$@"
echo '$ ./configure '"$@"
./configure "$@"
echo '$ make coqlight'
make coqlight
echo '$ sudo make install-coqlight install-devfiles'
@@ -41,4 +41,4 @@ fi
# or using more evil (but portable) 'eval', do
# $ eval 'exec "$COQTOP" '"$COQ_ARGS"' "$@"'
# Instead, we duplicate code, because it's simpler.
exec "$mythmdepdir/coqthmdep" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
exec "$mythmdepdir/coqthmdep" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
@@ -49,4 +49,4 @@ else
export HOTTLIB="@hottdir@/theories"
export HOTTCONTRIB="@hottdir@/contrib"
fi
#export COQ_ARGS=(-no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter)
#export COQ_ARGS=(-coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter)
2 hoqc
@@ -46,4 +46,4 @@ fi
# or using more evil (but portable) 'eval', do
# $ eval 'exec "$COQC" '"$COQ_ARGS"' "$@"'
# Instead, we duplicate code, because it's simpler.
exec "$COQC" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
exec "$COQC" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
2 hoqdep
@@ -46,4 +46,4 @@ fi
# or using more evil (but portable) 'eval', do
# $ eval 'exec "$COQDEP" '"$COQ_ARGS"' "$@"'
# Instead, we duplicate code, because it's simpler.
exec "$COQDEP" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
exec "$COQDEP" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
2 hoqide
@@ -46,4 +46,4 @@ fi
# or using more evil (but portable) 'eval', do
# $ eval 'exec "$COQIDE" '"$COQ_ARGS"' "$@"'
# Instead, we duplicate code, because it's simpler.
exec "$COQIDE" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
exec "$COQIDE" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
2 hoqtop
@@ -46,4 +46,4 @@ fi
# or using more evil (but portable) 'eval', do
# $ eval 'exec "$COQTOP" '"$COQ_ARGS"' "$@"'
# Instead, we duplicate code, because it's simpler.
exec "$COQTOP" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
exec "$COQTOP" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
@@ -46,4 +46,4 @@ fi
# or using more evil (but portable) 'eval', do
# $ eval 'exec "$COQTOP.byte" '"$COQ_ARGS"' "$@"'
# Instead, we duplicate code, because it's simpler.
exec "$COQTOP.byte" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
exec "$COQTOP.byte" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"

0 comments on commit 88ed234

Please sign in to comment.
You can’t perform that action at this time.