Opened 14 years ago

Closed 13 years ago

#26448 closed defect (invalid)

install coq fails in configuring stage

Reported by: thomas.anberree@… Owned by: reilles@…
Priority: Normal Milestone:
Component: ports Version: 1.9.1
Keywords: Cc:
Port: coq

Description (last modified by ryandesign (Ryan Carsten Schmidt))

Hi, Working with OS X 10.6.4. Following instructions "Installing Coq 8.2pl1 on Macintosh" on webpage

http://www.cs.princeton.edu/courses/archive/fall09/cos441/coq-mac.html

failed at step 12 with the following output:

sudo port install coq build.cmd=/opt/local/bin/gmake 
--->  Computing dependencies for coq
--->  Fetching coq
--->  Attempting to fetch coq-8.2pl1.tar.gz from http://aarnet.au.distfiles.macports.org/pub/macports/distfiles/coq
--->  Verifying checksum(s) for coq
--->  Extracting coq
--->  Applying patches to coq
--->  Configuring coq
Error: Target org.macports.configure returned: configure failure: shell command failed
Log for coq is at: /opt/local/var/macports/logs/_opt_local_var_macports_sources_rsync.macports.org_relse_ports_lang_coq/main.log
Error: Status 1 encountered during processing.
To report a bug, see <http://guide.macports.org/#project.tickets>

Change History (3)

comment:1 Changed 14 years ago by ryandesign (Ryan Carsten Schmidt)

Description: modified (diff)
Keywords: coq 8.2pl1 removed
Owner: changed from macports-tickets@… to reilles@…
Port: coq added

Please use WikiFormatting, fill in the Port field, and Cc the port's maintainer.

You need to supply the main.log file referenced, otherwise we can't know what went wrong.

I don't know what this "build.cmd=/opt/local/bin/gmake" is. I'd say don't do that, and don't make a symlink /opt/local/bin/make either. I don't know why we need a 14-step tutorial when as far as I can tell it's just one step: "sudo port install coq". It installs fine for me when I just do that. I don't know why that tutorial you found wants you to jump through hoops. If they think there's something wrong with just running "sudo port install coq" they should file a bug report with us rather than write up strange workarounds.

comment:2 in reply to:  description Changed 13 years ago by kb.common+macports@…

Replying to thomas.anberree@…:

Hi, Working with OS X 10.6.4. Following instructions "Installing Coq 8.2pl1 on Macintosh" on webpage

http://www.cs.princeton.edu/courses/archive/fall09/cos441/coq-mac.html

I see that coq requires both ocaml and camlp5, hence this bug might just be duplicate of (dependent on?) 26769.

To see if that is the case check the version of camplp5. It should be something like this:

$ camlp5 -v
Camlp5 version 5.15 (ocaml 3.12.0)

If instead it says, Camlp5 version 5.14 (ocaml 3.12.0) or any pair of incompatible versions you will have to wait till the ports are updated.

A workaround until then is to uninstall the camlp5 from port and install manually from http://pauillac.inria.fr/~ddr/camlp5/. See INSTALL file in the archive.

For me it looked something like,

$ port uninstall camlp5
< download and extract file from inria.fr >
< change to that directory >
$ ./configure --prefix /usr/local --transitional
$ make world.opt
$ sudo make install

comment:3 Changed 13 years ago by jmroot (Joshua Root)

Resolution: invalid
Status: newclosed

No log, no way of knowing what the problem was.

Note: See TracTickets for help on using tickets.