Dear Mark,
This (HOLDIR being hardcoded) is a known (but previously undocumented
outside of private emails) issue.
I have created an issue for it, and some of the discussion about how to fix
it and hard problems:
https://github.com/mn200/HOL/issues/105
I am also interested in making HOL4 installable after building so I can
make a package for Parabola (and Arch Linux).
Your second issue about executable stack markings I'm less familiar with.
Have you submitted your polyml patch upstream?
What is the right way to fix it? Do we just need -Wa,--noexecstack to be
passed at all times to poly during the build?
Is it suitable for non-GNU-based systems? Perhaps I leave this one for you
to sort out by patching for Gentoo.
I guess you need help tracking down other ways in which executables are
created during the build process? (It might be a bug that machine_flags
doesn't catch them all.)
Cheers,
Ramana
On Sat, Dec 22, 2012 at 11:48 AM, Mark Wright <[email protected]> wrote:
> Hi,
>
> I tried to create a sci-mathematics/hol4-kananaskis-8 ebuild for
> Gentoo:
>
>
> http://dev.gentoo.org/~gienah/hol4/sci-mathematics/hol4-kananaskis/hol4-kananaskis-8.ebuild
>
> http://dev.gentoo.org/~gienah/hol4/sci-mathematics/hol4-kananaskis/files/hol4-kananaskis-8-config.patch
>
> http://dev.gentoo.org/~gienah/hol4/sci-mathematics/hol4-kananaskis/files/50hol4-kananaskis-gentoo.el
>
> An ebuild is a bash script that is used to compile a package from the
> source code for Gentoo (a source code based free linux distribution).
>
> As is the case with most operating system packaging, to create a package
> it is necessary to:
>
> - patch the package if necessary. This is the src_prepare phase in
> hol4-kananaskis-8.ebuild
>
> For Gentoo it is necessary to specify the user's linker flags, LDFLAGS,
> so for that I patch tools-poly/configure.sml to be in a form that is
> easier to manipulate with sed, then use sed to specify the LDFLAGS.
>
> - configure the package, where the installation prefix is specified.
> This is the src_configure phase.
>
> So I follow the instructions in INSTALL, and specify the holdir
> in tools-poly/poly-includes.ML like:
>
> val holdir = "/usr/share/hol-kananaskis-8"
>
> In the build.log though this appears to be ignored:
>
> >>> Configuring source in
> /h/argus/3/root/var/tmp/portage/sci-mathematics/hol4-kananaskis-8/work/hol-kananaskis-8
> ...
> Poly/ML 5.5.0 Release
> > # # # # # # # # # # #
> HOL smart configuration.
>
> [Using override file tools-poly/poly-includes.ML]
>
> Determining configuration parameters: holdir OS poly polymllibdir
> OS: linux
> poly: /usr/bin/poly
> polymllibdir: /usr/lib64
> holdir:
> /h/argus/3/root/var/tmp/portage/sci-mathematics/hol4-kananaskis-8/work/hol-kananaskis-8
>
> - compile it one directory. This is the src_compile phase.
>
> There are 1000s of files that contain hardcoded paths to the directory
> where the sources are being compiled.
>
> - run the tests if they can be persuaded to compile, run and pass. This is
> the src_test phase.
>
> I don't know how to run the tests or if there are any.
>
> - then install it, in this step the installation prefix can be specified
> again
> if you like. This is the src_install phase.
>
> I could not see any installation method provided, so I try to patch
> the hardcoded paths in the text files and copy them to the final location.
>
> The result though is that hol4 is totally broken and I can not see
> any way to package this on Gentoo without help. Running it fails:
>
> % hol
> /usr/bin/hol: line 5:
> /h/argus/3/root/var/tmp/portage/sci-mathematics/hol4-kananaskis-8/work/hol-kananaskis-8/bin/hol.builder:
> Permission denied
>
> I killed the hol process.
>
> % /usr/share/hol-kananaskis-8/bin/heapname
>
> /h/argus/3/root/var/tmp/portage/sci-mathematics/hol4-kananaskis-8/work/hol-kananaskis-8/bin/hol.builder
> %
>
> So I try replacing heapname with a script:
>
> argus% cat /usr/share/hol-kananaskis-8/bin/heapname
> #! /bin/sh
>
> echo "/usr/share/hol-kananaskis-8/bin/hol.builder"
> argus% /usr/share/hol-kananaskis-8/bin/heapname
> /usr/share/hol-kananaskis-8/bin/hol.builder
> argus% hol
>
> ---------------------------------------------------------------------
> HOL-4 [Kananaskis 8 (stdknl, )]
>
> For introductory HOL help, type: help "hol";
> ---------------------------------------------------------------------
>
> Exception- Io {name =
> "/h/argus/3/root/var/tmp/portage/sci-mathematics/hol4-kananaskis-8/work/hol-kananaskis-8/tools/Holmake/internal_functions.sig",
> cause = SysErr ("Permission denied", SOME EACCES), function =
> "TextIO.openIn"} raised
>
>
> I packaged Isabelle on Gentoo, a very difficult package. I could package
> hol4 if there was *any* way to do it. As in:
>
> - patching it
>
> - updating/replacing the entire build system with a patch or tarball
>
> - updating hol4-kananaskis to a new version
>
> - sed stuff
>
> - specifying the installation prefix in any way in any or all of the
> src_configure, src_compile, src_install steps.
>
> - compiling it with a different standard ML compiler, like MLton, if
> similar or better performance than polyml can be achieved.
>
> - any combination of the above, regardless of how much of a hack it is.
>
> Of course it is necessary that everything works though, including Holmake,
> and the documentation hyperlinks.
>
> Currently I have another problem as well: I get these QA errors:
>
> * QA Notice: The following files contain writable and executable sections
> * Files with such sections will not work properly (or at all!) on some
> * architectures/operating systems. A bug should be filed at
> * http://bugs.gentoo.org/ to make sure the issue is fixed.
> * For more information, see http://hardened.gentoo.org/gnu-stack.xml
> * Please include the following list of files in your report:
> * Note: Bugs should be filed for the respective maintainers
> * of the package in question and not [email protected].
> * RWX --- --- usr/bin/Holmake
> * RWX --- --- usr/share/hol-kananaskis-8/bin/heapname
> * RWX --- --- usr/share/hol-kananaskis-8/bin/build
> * RWX --- --- usr/share/hol-kananaskis-8/bin/unquote
> * RWX --- --- usr/share/hol-kananaskis-8/bin/hol.builder0
> * RWX --- --- usr/share/hol-kananaskis-8/bin/mkmunge.exe
> * RWX --- --- usr/share/hol-kananaskis-8/bin/hol.builder
> * RWX --- --- usr/share/hol-kananaskis-8/src/num/termination/numheap
> * RWX --- --- usr/share/hol-kananaskis-8/src/TeX/mkmunge.exe
> * !WX --- --- usr/share/hol-kananaskis-8/src/TeX/mkmunge.o
> * RWX --- --- usr/share/hol-kananaskis-8/tools/mllex/mllex.exe
> * RWX --- --- usr/share/hol-kananaskis-8/tools/mlyacc/src/mlyacc.exe
> * RWX --- --- usr/share/hol-kananaskis-8/help/src-sml/makebase.exe
> * RWX --- --- usr/share/hol-kananaskis-8/help/src-sml/Doc2Txt.exe
> * RWX --- --- usr/share/hol-kananaskis-8/help/src-sml/Doc2Html.exe
> * RWX --- --- usr/share/hol-kananaskis-8/help/src-sml/Doc2Tex.exe
>
> I already tried patching -Wa,--noexecstack into machine_flags in
> tools-poly/configure.sml:
>
> val machine_flags = ["-Wl,--hash-style=gnu", "-Wl,-O1", "-Wl,--as-needed",
> "-Wa,--noexecstack"]
>
> I patched polyml:
>
> --- polyml.5.5-orig/libpolyml/x86asm.asm 2012-05-03
> 21:07:59.000000000 +1000
> +++ polyml.5.5/libpolyml/x86asm.asm 2012-09-19 17:41:51.767737295 +1000
> @@ -3003,4 +3003,7 @@
> dd Mask_assign_byte ;# 254
> dd Mask_assign_word ;# 255
>
> +#if defined(__linux__) && defined(__ELF__)
> +.section .note.GNU-stack,"",%progbits
> +#endif
> END
>
> I could try some other things, like:
>
> - trying to splice "-Wa,--noexecstack" into some other flags.
>
> - patching or linking in some assembler code.
>
> Thanks, Mark
>
>
> ------------------------------------------------------------------------------
> LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
> Remotely access PCs and mobile devices and provide instant support
> Improve your efficiency, and focus on delivering more value-add services
> Discover what IT Professionals Know. Rescue delivers
> http://p.sf.net/sfu/logmein_12329d2d
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
Remotely access PCs and mobile devices and provide instant support
Improve your efficiency, and focus on delivering more value-add services
Discover what IT Professionals Know. Rescue delivers
http://p.sf.net/sfu/logmein_12329d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
