search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

fails to build, involves Bool.v and Nativevalues #201

Closed DanGrayson closed 11 years ago

DanGrayson commented 11 years ago

Any ideas?

/Users/dan/src/coq-builder/encap-2/coq84hoq-8.4hoq/bin/coqtop -indices-matter -boot -nois -coqlib ./coq -R ./coq/theories Coq -compile coq/theories/Bool/Bool File "/Users/dan/src/UnivalentFoundations/github/DanGrayson/HoTT/coq/theories/Bool/NCoq_Bool_Bool.ml", line 1, characters 0-17: Error: Unbound module Nativevalues Warning: Removed file /Users/dan/src/UnivalentFoundations/github/DanGrayson/HoTT/coq/theories/Bool/Bool.vo Anomaly: Library compilation failure. Please report. Makefile:681: recipe for target 'coq/theories/Bool/Bool.vo' failed

JasonGross commented 11 years ago

Is this on master? Do you know which commit introduced it (or how to get git blame to tell you)? This is the error that I am getting when I try to bundle coq, but which I do not get with my installed coq.

DanGrayson commented 11 years ago

Yes, it's on master, and I haven't been making regularly, so it's hard to say when it started. If you're getting it, too, then I'll try to figure it out!

JasonGross commented 11 years ago

Adding a symlink to kernel (in addition to dev and plugins) makes it complain about Declaremods. Additionally adding a symlink to library makes it go through.

JasonGross commented 11 years ago

Does #202 fix this for you?

DanGrayson commented 11 years ago

Yes, but it seems to insist on building coq for me, which I prefer to do myself.

On Mon, Aug 26, 2013 at 9:50 PM, Jason Gross notifications@github.comwrote:

Does #202 https://github.com/HoTT/HoTT/issues/202 fix this for you?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/201#issuecomment-23308115 .

DanGrayson commented 11 years ago

This worked:

diff --git a/configure.ac b/configure.ac
index b6c878e..f8fdd23 100644
--- a/configure.ac
+++ b/configure.ac
@@ -184,8 +184,8 @@ AC_MSG_NOTICE([Creating symbolic links into Coq standard library.])
 # We must have these links in the source directory, not in the build
 # directory, because the replacement standard library lives in the source
 # directory, and these links are required to make Coq accept it.
-rm -f $srcdir/coq/plugins $srcdir/coq/dev
-ln -s $COQLIB/plugins $COQLIB/dev $srcdir/coq
+rm -f $srcdir/coq/plugins $srcdir/coq/dev $srcdir/coq/kernel $srcdir/coq/library
+ln -s $COQLIB/plugins $COQLIB/dev $COQLIB/kernel $COQLIB/library $srcdir/coq
 # TODO(jgross): Should we use AC_CONFIG_LINKS?  But $COQLIB/dev
 # doesn't exist in my installation, and that would make configure
 # error...
peterlefanulumsdaine commented 11 years ago

I’m getting this issue, or a superficially very similar one, on the current master, after following the Quick Installation instructions from INSTALL.txt:

[…]/HoTT/coq-HoTT/bin/coqtop -indices-matter -boot -nois -coqlib ./coq -R ./coq/theories Coq -compile coq/theories/Bool/Bool
Warning: Cannot open ./coq/dev
Warning: Cannot open ./coq/plugins
File "[…]/HoTT/coq/theories/Bool/NCoq_Bool_Bool.ml", line 1, characters 0-17:
Error: Unbound module Nativevalues
Warning:
Removed file […]/HoTT/coq/theories/Bool/Bool.vo
Anomaly: Library compilation failure. Please report.
make: *** [coq/theories/Bool/Bool.vo] Error 1
Peter-LeFanu-Lumsdaines-MacBook:HoTT peterlefanulumsdaine$

(Long paths above abridged by hand). This happens even on a clean clone of the whole repo. It appears that something is looking in coq/dev and coq/plugins; however, the automated install of Coq given by ./etc/install_coq.sh has not created such directories:

Peter-LeFanu-Lumsdaines-MacBook:HoTT peterlefanulumsdaine$ ls coq theories tools

The normal coq directory structure, including dev and plugins, is all present, but under coq-HoTT not under coq.

JasonGross commented 11 years ago

The error messages given could either mean that the symlinks don't exist, or that they don't point to valid directories. The automated install of Coq given by ./etc/install_coq.sh does not create the symlinks; ./configure does. After you run ./autogen.sh and ./configure, and then ls coq, you should have the symlinks. Is this the case? If not, there's something going wrong with configure or autoreconf, which is worrisome (and if you paste the full output of ./autgen.sh && ./configure COQBIN="$(pwd)/coq-HoTT/bin" (after having already run ./etc/install_coq.sh) perhaps I will have more ideas). If the symlinks are there, can you tell me where they point (with ls -la coq)? They should point to, e.g., […]/HoTT/coq-HoTT/dev.

peterlefanulumsdaine commented 11 years ago

The symlinks don’t seem to be present at all. Full output as requested; I guess it looks like at the stage of creating the symlinks, the name-generation is going wrong, and configure is trying to create all the links just as ./coq//?

Peter-LeFanu-Lumsdaines-MacBook:HoTT peterlefanulumsdaine$ sudo ./autogen.sh && ./configure COQBIN="$(pwd)/coq-HoTT/bin"
autoreconf: Entering directory `.'
autoreconf: configure.ac: not using Gettext
autoreconf: running: aclocal --force -I etc
autoreconf: configure.ac: tracing
autoreconf: configure.ac: not using Libtool
autoreconf: running: /sw/bin/autoconf-2.69 --force
autoreconf: configure.ac: not using Autoheader
autoreconf: running: automake --add-missing --copy --force-missing
autoreconf: Leaving directory `.'
checking whether to enable maintainer-specific portions of Makefiles... no
checking for a BSD-compatible install... /usr/bin/install -c
checking whether build environment is sane... yes
checking for a thread-safe mkdir -p... etc/install-sh -c -d
checking for gawk... no
checking for mawk... no
checking for nawk... no
checking for awk... awk
checking whether make sets $(MAKE)... yes
checking whether ln -s works... yes
checking whether make sets $(MAKE)... (cached) yes
configure: Will first look for Coq executables in /[…]/HoTT/coq-HoTT/bin
checking for coqtop... /[…]/HoTT/coq-HoTT/bin/coqtop
checking coqtop version... trunk
checking Coq library path... /[…]/HoTT/coq-HoTT
configure: COQBIN is /[…]/HoTT/coq-HoTT/bin
checking for coqc... /[…]/HoTT/coq-HoTT/bin/coqc
checking coqc version... trunk
configure: Will not compile ssreflect
checking for coqide... no
configure: Could not find coqide, will not make hoqide
checking for coqdep... /[…]/HoTT/coq-HoTT/bin/coqdep
checking for coqdoc... /[…]/HoTT/coq-HoTT/bin/coqdoc
checking for coq_makefile... /[…]/HoTT/coq-HoTT/bin/coq_makefile
checking for etags... etags
checking for time... /usr/bin/time
configure: Creating symbolic links into Coq standard library
ln: ./coq//: File exists
ln: ./coq//: File exists
ln: ./coq//: File exists
ln: ./coq//: File exists
configure: creating ./config.status
config.status: creating Makefile
config.status: creating hoq-config
Peter-LeFanu-Lumsdaines-MacBook:HoTT peterlefanulumsdaine$ ls coq
theories    tools
JasonGross commented 11 years ago

Try changing

rm -f "$srcdir/coq/dev" "$srcdir/coq/kernel" "$srcdir/coq/library" "$srcdir/coq/plugins"
ln -s "$COQLIB/dev/" "$COQLIB/kernel/" "$COQLIB/library/" "$COQLIB/plugins/" "$srcdir/coq/"

to

echo "rm -f '$srcdir/coq/dev' '$srcdir/coq/kernel' '$srcdir/coq/library' '$srcdir/coq/plugins'"
rm -f "$srcdir/coq/dev" "$srcdir/coq/kernel" "$srcdir/coq/library" "$srcdir/coq/plugins"
echo "ln -s '$COQLIB/dev/' '$COQLIB/kernel/' '$COQLIB/library/' '$COQLIB/plugins/' '$srcdir/coq/'"
ln -s "$COQLIB/dev/" "$COQLIB/kernel/" "$COQLIB/library/" "$COQLIB/plugins/" "$srcdir/coq/"

(I just inserted the two echo lines) and running ./autgen.sh && ./configure COQBIN="$(pwd)/coq-HoTT/bin" again, and let me know what the output is between "configure: Creating symbolic links into Coq standard library" and "configure: creating ./config.status".

Also, what system are you running this on, and what happens when you run the following commands?

pushd /tmp
mkdir testhott
cd testhott
mkdir a
mkdir b
mkdir c
mkdir d
ln -s ./a/ ./b/ ./c/
ls c
ln -s ./a ./b ./d/
ls d
popd
peterlefanulumsdaine commented 11 years ago

With the echo lines added, that section of the output is (again with local paths abridged):

configure: Creating symbolic links into Coq standard library
rm -f './coq/dev' './coq/kernel' './coq/library' './coq/plugins'
ln -s '/[…]/HoTT/coq-HoTT/dev/' '/[…]/HoTT/coq-HoTT/kernel/' '/[…]/HoTT/coq-HoTT/library/' '/[…]/HoTT/coq-HoTT/plugins/' './coq/'
ln: ./coq//: File exists
ln: ./coq//: File exists
ln: ./coq//: File exists
ln: ./coq//: File exists
configure: creating ./config.status

I’m on Mac OS 10.8.5; the output of your small testing script is:

Peter-LeFanu-Lumsdaines-MacBook:tmp peterlefanulumsdaine$ mkdir testhott
Peter-LeFanu-Lumsdaines-MacBook:tmp peterlefanulumsdaine$ cd testhott
Peter-LeFanu-Lumsdaines-MacBook:testhott peterlefanulumsdaine$ mkdir a
Peter-LeFanu-Lumsdaines-MacBook:testhott peterlefanulumsdaine$ mkdir b
Peter-LeFanu-Lumsdaines-MacBook:testhott peterlefanulumsdaine$ mkdir c
Peter-LeFanu-Lumsdaines-MacBook:testhott peterlefanulumsdaine$ mkdir d
Peter-LeFanu-Lumsdaines-MacBook:testhott peterlefanulumsdaine$ ln -s ./a/ ./b/ ./c/
ln: ./c//: File exists
ln: ./c//: File exists
Peter-LeFanu-Lumsdaines-MacBook:testhott peterlefanulumsdaine$ ls c
Peter-LeFanu-Lumsdaines-MacBook:testhott peterlefanulumsdaine$ ln -s ./a ./b ./d/
Peter-LeFanu-Lumsdaines-MacBook:testhott peterlefanulumsdaine$ ls d
a   b

And, as that suggests, removing the trailing slashes in the ln -s line of configure.ac, i.e. changing it to

ln -s "$COQLIB/dev" "$COQLIB/kernel" "$COQLIB/library" "$COQLIB/plugins" "$srcdir/coq"

seems to fix the whole issue: with that change, the library builds fine for me!