Menu
▾
▴
[Hol-info] hol4 relocatable build
|
From: Mark W. <gi...@ge...> - 2012-12-22 00:48:42
|
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 hardened@g.o. * 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 |
