Bug 166867 - update port and fix build: math/proofgeneral
Summary: update port and fix build: math/proofgeneral
Status: Closed FIXED
Alias: None
Product: Ports & Packages
Classification: Unclassified
Component: Individual Port(s) (show other bugs)
Version: Latest
Hardware: Any Any
: Normal Affects Only Me
Assignee: Michael Scheidell
URL:
Keywords:
Depends on:
Blocks:
 
Reported: 2012-04-12 09:50 UTC by Timothy Beyer
Modified: 2012-04-19 23:41 UTC (History)
1 user (show)

See Also:


Attachments
proofgeneral.diff (52.81 KB, patch)
2012-04-12 09:50 UTC, Timothy Beyer
no flags Details | Diff
Makefile (2.01 KB, text/plain)
2012-04-16 01:12 UTC, Michael Scheidell
no flags Details

Note You need to log in before you can comment on or make changes to this bug.
Description Timothy Beyer 2012-04-12 09:50:12 UTC
- Update port to version 4.1

- Fix build on amd64 (and likely all other architectures)

- XEmacs is no longer supported by proofgeneral developers, so only GNU Emacs may be used

- simplify some of the patches by using MAKE_ARGS when possible.

- get rid of USE_GNOME, since there is nothing Gnome related about this port

- Omit Pdf compilation

Explanation:

Due to recent changes to the port print/texinfo, math/proofgeneral (3.7.1) no
longer compiles properly.  (due to issues compiling the info files with the
newer texinfo) The new version of math/proofgeneral (this one) does not have
this issue, because it works with recent versions of texinfo, as it should.

However, the pdf compilation in the newest version requires a newer version of
latex than what is available in the tetex distribution.  (the latex in texlive
would be sufficient if that feature is desired) Therefore, pdf compilation is
ommitted, due to this issue.

This is a fairly important update, because the current version in ports no
longer compiles, according to error logs on portsmon.

Fix: Apply the patch and build
How-To-Repeat: apply the patch and build
Comment 1 Michael Scheidell freebsd_committer 2012-04-15 21:56:57 UTC
Responsible Changed
From-To: freebsd-ports-bugs->scheidell

I'll take it.
Comment 2 Michael Scheidell freebsd_committer 2012-04-16 00:26:44 UTC
State Changed
From-To: open->feedback

Thank you for your support of FreeBSD and your continued maintaince of this port. 
A couple of issues. 

<http://people.freebsd.org/~scheidell/proofgeneral-emacs-4.1.log 

your patch with !NOPORTDOCS looks for texi2html, and pulls in texinfo 
(which was already installed earlier, line 505), so, this causes a failure at line 1474. 
.if !defined(NOPORTDOCS) 
MAKE_ARGS+=     DOCSDIR=${DOCSDIR} INSTALLDOC=install-doc 
BUILD_DEPENDS+= texi2html:${PORTSDIR}/print/texinfo 
.endif 

did you mean to install texi2html port? 

/usr/ports/textproc/texi2html 

or is texi2html needed to build this? 

minor issues: 

I renamed the patch files back to their original names.  this helps preserve cvs history. 

FATAL: file files/patch-doc_Makefile.doc not in CVS. 
FATAL: file files/patch-isar_interface not in CVS. 
FATAL: CVS file files/patch-doc-Makefile.doc missing 
FATAL: CVS file files/patch-isar-interface missing 

I moved PKGNAMESUFFIX 'up' to where it belongs (should not affect anything) and changed the += to an =  

and, changed the BUILD_DEPENDS/RUN_DEPENDS += to = (this is not a master port, is it?, slave of something else?) 

last minor issue:  (i build embedded systems, so look at the NOPORTDOCS carefully) 
Have you considered using the more modern use of the PORTDOCS= macros? 
look at some of the newest examples?  join and post to freebsd-port and ask. 
You can totally eliminate the %%PORTDOCS%%%%DOCSDIR%% lines in pkg-plist.  Makes for easier upgrades. 

Fix texi2html (let me know if you need it, really) and experiment with the PORTDOCS= macro in Makefile. 
If you want this committed without the new PORTDOCS= stuff, that is fine, just lets leave the pr open because the ports audit  
comittee is going to ping me about it otherwise. 

Thanks again.
Comment 3 Michael Scheidell freebsd_committer 2012-04-16 01:12:58 UTC
yep, it looks like you should use the macro version of PORTDOCS=

install -o root -g wheel -m 444 doc/proofgeneral.1 /usr/local/man/man1
803     install -o root -g wheel -m 444 doc/PG-adapting.info /usr/local/info
804     install -o root -g wheel -m 444 doc/ProofGeneral.info /usr/local/info
805     mkdir -p /usr/local/share/doc/proofgeneral
806     for f in AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER; do install -o root -g wheel -m 444 $f 
/usr/local/share/doc/proofgeneral; done
807     for f in acl2/*.acl2 hol98/*.sml isar/*.thy lclam/*.lcm lego/*.l pgshell/*.pgsh phox/*.phx plastic/*.lf twelf/*.elf; 
do mkdir -p /usr/local/share/doc/proofgeneral/`dirname $f`; \
808     install -o root -g wheel -m 444 $f /usr/local/share/doc/proofgeneral/$f; done
809     install: lclam/*.lcm: No such file or directory
810     install: plastic/*.lf: No such file or directory

something like:
PORTDOCS= AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER \
                        acl2/*.acl2 hol98/*.sml isar/*.thy (etc)

and, like I said, you don't need the entries in pkg-plist.  they would be automatic.

as hinted in first feedback, I 'touched' your Makefile.
This one has a BUILD_DEPENDS+= texi2html that seems to work better, and has those minor thing (other than PORTDOCS MACRO) as 
mentioned.

If you like, you can just attach to the pr patches to this Makefile, or a whole Makefile, and a whole pkg-plist.

Thanks again for your work.
-- 
Michael Scheidell, CTO
SECNAP Network Security Corporation
http://people.freebsd.org/~scheidell

______________________________________________________________________
This email has been scanned and certified safe by SpammerTrap(r). 
For Information please see http://www.spammertrap.com/
______________________________________________________________________  
  
Comment 4 Timothy Beyer 2012-04-17 01:08:21 UTC
Hi,

The diffs are indented to be applied against my original submission, since the
Makefile.diff incorporates your fixes.  Support for the PORTDOCS macro was
added to the Makefile on top of the fixes, and the pkg-plist no longer contains
documentation files or directories.

If there is anything else that needs to be addressed, I can send patches as
needed.

Regards,
Tim

--- Makefile.diff begins here ---
--- Makefile.orig	2012-04-12 00:11:12.000000000 -0700
+++ Makefile	2012-04-16 16:52:46.000000000 -0700
@@ -9,6 +9,7 @@
 PORTVERSION=	4.1
 CATEGORIES=	math elisp
 MASTER_SITES=	http://proofgeneral.inf.ed.ac.uk/releases/
+PKGNAMESUFFIX=	-${EMACS_NAME}
 DISTNAME=	ProofGeneral-${PORTVERSION}
 EXTRACT_SUFX=	.tgz
 
@@ -18,10 +19,8 @@
 LICENSE=	GPLv2
 LICENSE_FILE=	${WRKSRC}/COPYING
 
-PKGNAMESUFFIX+=	-${EMACS_NAME}
-
-BUILD_DEPENDS+=	bash:${PORTSDIR}/shells/bash
-RUN_DEPENDS+=	${LOCALBASE}/share/icons/hicolor/index.theme:${PORTSDIR}/misc/hicolor-icon-theme
+BUILD_DEPENDS=	bash:${PORTSDIR}/shells/bash
+RUN_DEPENDS=	${LOCALBASE}/share/icons/hicolor/index.theme:${PORTSDIR}/misc/hicolor-icon-theme
 
 USE_EMACS=	yes
 USE_GMAKE=	yes
@@ -49,9 +48,13 @@
 
 .if !defined(NOPORTDOCS)
 MAKE_ARGS+=	DOCSDIR=${DOCSDIR} INSTALLDOC=install-doc
-BUILD_DEPENDS+=	texi2html:${PORTSDIR}/print/texinfo
+BUILD_DEPENDS+=	texi2html:${PORTSDIR}/textproc/texi2html
 .endif
 
+PORTDOCS=	AUTHORS BUGS CHANGES COMPATIBILITY COPYING INSTALL \
+	PG-adapting ProofGeneral README REGISTER acl2 hol98 isar lclam lego \
+	pgshell phox plastic twelf
+
 post-patch:
 	@${REINPLACE_CMD} -e 's,%%PREFIX%%,${PREFIX},' \
 		${WRKSRC}/etc/desktop/proofgeneral.desktop
--- Makefile.diff ends here ---

--- pkg-plist.diff begins here ---
--- pkg-plist.orig	2012-04-12 00:22:43.000000000 -0700
+++ pkg-plist	2012-04-16 16:36:30.000000000 -0700
@@ -4,76 +4,6 @@
 bin/proofgeneral
 share/application-registry/proofgeneral.applications
 share/applications/proofgeneral.desktop
-%%PORTDOCS%%%%DOCSDIR%%/AUTHORS
-%%PORTDOCS%%%%DOCSDIR%%/BUGS
-%%PORTDOCS%%%%DOCSDIR%%/CHANGES
-%%PORTDOCS%%%%DOCSDIR%%/COMPATIBILITY
-%%PORTDOCS%%%%DOCSDIR%%/COPYING
-%%PORTDOCS%%%%DOCSDIR%%/INSTALL
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_1.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_10.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_11.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_12.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_13.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_14.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_15.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_16.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_17.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_18.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_19.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_2.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_3.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_4.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_5.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_6.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_7.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_8.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_9.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_abt.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_toc.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_1.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_10.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_11.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_12.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_13.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_14.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_15.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_16.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_17.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_18.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_19.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_2.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_20.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_21.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_22.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_23.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_3.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_4.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_5.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_6.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_7.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_8.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_9.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_abt.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_fot.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_toc.html
-%%PORTDOCS%%%%DOCSDIR%%/README
-%%PORTDOCS%%%%DOCSDIR%%/REGISTER
-%%PORTDOCS%%%%DOCSDIR%%/acl2/example.acl2
-%%PORTDOCS%%%%DOCSDIR%%/acl2/root2.acl2
-%%PORTDOCS%%%%DOCSDIR%%/hol98/example.sml
-%%PORTDOCS%%%%DOCSDIR%%/hol98/root2.sml
-%%PORTDOCS%%%%DOCSDIR%%/isar/Example-Tokens.thy
-%%PORTDOCS%%%%DOCSDIR%%/isar/Example.thy
-%%PORTDOCS%%%%DOCSDIR%%/lego/example.l
-%%PORTDOCS%%%%DOCSDIR%%/lego/example2.l
-%%PORTDOCS%%%%DOCSDIR%%/lego/root2.l
-%%PORTDOCS%%%%DOCSDIR%%/pgshell/example.pgsh
-%%PORTDOCS%%%%DOCSDIR%%/phox/example.phx
-%%PORTDOCS%%%%DOCSDIR%%/phox/square-root-2.phx
-%%PORTDOCS%%%%DOCSDIR%%/twelf/example.elf
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/acl2/acl2.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/acl2/acl2.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/ccc/ccc.el
@@ -323,18 +253,6 @@
 @dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/ccc
 @dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/acl2
 @dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral
-%%PORTDOCS%%@dirrm %%DOCSDIR%%/twelf
-%%PORTDOCS%%@dirrm %%DOCSDIR%%/plastic
-%%PORTDOCS%%@dirrm %%DOCSDIR%%/phox
-%%PORTDOCS%%@dirrm %%DOCSDIR%%/pgshell
-%%PORTDOCS%%@dirrm %%DOCSDIR%%/lego
-%%PORTDOCS%%@dirrm %%DOCSDIR%%/lclam
-%%PORTDOCS%%@dirrm %%DOCSDIR%%/isar
-%%PORTDOCS%%@dirrm %%DOCSDIR%%/hol98
-%%PORTDOCS%%@dirrm %%DOCSDIR%%/acl2
-%%PORTDOCS%%@dirrm %%DOCSDIR%%/ProofGeneral
-%%PORTDOCS%%@dirrm %%DOCSDIR%%/PG-adapting
-%%PORTDOCS%%@dirrm %%DOCSDIR%%
 @dirrmtry share/applications
 @dirrmtry share/application-registry
 @dirrmtry share/pixmaps
--- pkg-plist.diff ends here ---
Comment 5 dfilter service freebsd_committer 2012-04-19 23:38:40 UTC
scheidell    2012-04-19 22:38:31 UTC

  FreeBSD ports repository

  Modified files:
    math/proofgeneral    Makefile distinfo pkg-plist 
    math/proofgeneral/files patch-Makefile patch-doc-Makefile.doc 
                            patch-etc_desktop_proofgeneral.desktop 
                            patch-isar-interface 
  Log:
  - Update to 4.1
  - Fix build on amd64
  - XEmacs is no longer supported by proofgeneral developers, so only GNU Emacs may be used
  - Omit pdf compilation since a newer version of latex then is in ports is needed
  - Use PORTDOCS= macros to simplefy Makefile and pkg-plist
  
  PR:             ports/166867
  Submitted by:   Timothy Beyer <beyert@cs.ucr.edu> (maintainer0
  
  Revision  Changes    Path
  1.28      +27 -32    ports/math/proofgeneral/Makefile
  1.9       +2 -2      ports/math/proofgeneral/distinfo
  1.8       +19 -87    ports/math/proofgeneral/files/patch-Makefile
  1.4       +57 -8     ports/math/proofgeneral/files/patch-doc-Makefile.doc
  1.3       +2 -2      ports/math/proofgeneral/files/patch-etc_desktop_proofgeneral.desktop
  1.2       +6 -6      ports/math/proofgeneral/files/patch-isar-interface
  1.11      +56 -375   ports/math/proofgeneral/pkg-plist
_______________________________________________
cvs-all@freebsd.org mailing list
http://lists.freebsd.org/mailman/listinfo/cvs-all
To unsubscribe, send any mail to "cvs-all-unsubscribe@freebsd.org"
Comment 6 Michael Scheidell freebsd_committer 2012-04-19 23:41:38 UTC
State Changed
From-To: feedback->closed

Committed, with minor changes. Thanks!