CakeML:5204c4cc4eadfc56cc83a3f0c7ef7208a8839def
Update .hol_preexec to not copy Holmakefile
#911 (libm_gen)
Merging into:68d5c7577d631f58bb40f40e1ebfe49873f26a38
Merge pull request #915 from CakeML/translator-fix
HOL:afad7a71de91823e350636ff17ada17e208032bf
Fix Unicode violation in previous
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 5s 124MB
Starting developers/bin
Finished developers/bin 5s 1GB
Starting floatingPoint/tools/dandelion
FAILED: floatingPoint/tools/dandelion
HOLORIG=/home/cug/hk324/cml-regression/cakeml-2063/floatingPoint/tools/dandelion tar -xf sollya-8.0.tar.gz sollya-8.0 &&\
cd sollya-8.0 &&\
./configure &&\
make &&\
rm -rf ./build-aux doc m4 tests-lib tests-tool &&\
rm -rf ./*.c ./*.h &&\
cd ../
checking for a BSD-compatible install... /usr/bin/install -c
checking whether build environment is sane... yes
checking for a race-free mkdir -p... /usr/bin/mkdir -p
checking for gawk... gawk
checking whether make sets $(MAKE)... yes
checking whether make supports nested variables... yes
checking whether to enable maintainer-specific portions of Makefiles... no
checking whether make supports nested variables... (cached) yes
checking for bison... no
checking for byacc... no
checking for gcc... gcc
checking whether the C compiler works... yes
checking for C compiler default output file name... a.out
checking for suffix of executables...
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether the compiler supports GNU C... yes
checking whether gcc accepts -g... yes
checking for gcc option to enable C11 features... none needed
checking whether gcc understands -c and -o together... yes
checking whether make supports the include directive... yes (GNU style)
checking dependency style of gcc... gcc3
checking how to run the C preprocessor... gcc -E
checking for g++... g++
checking whether the compiler supports GNU C++... yes
checking whether g++ accepts -g... yes
checking for g++ option to enable C++11 features... none needed
checking dependency style of g++... gcc3
checking for gawk... (cached) gawk
checking for a sed that does not truncate output... /usr/bin/sed
checking for ar... ar
checking the archiver (ar) interface... ar
checking whether C++ compiler works... yes
checking for flex... no
checking for lex... no
checking whether ln -s works... yes
checking whether make sets $(MAKE)... (cached) yes
checking build system type... x86_64-pc-linux-gnu
checking host system type... x86_64-pc-linux-gnu
checking how to print strings... printf
checking for a sed that does not truncate output... (cached) /usr/bin/sed
checking for grep that handles long lines and -e... /usr/bin/grep
checking for egrep... /usr/bin/grep -E
checking for fgrep... /usr/bin/grep -F
checking for ld used by gcc... /usr/bin/ld
checking if the linker (/usr/bin/ld) is GNU ld... yes
checking for BSD- or MS-compatible name lister (nm)... /usr/bin/nm -B
checking the name lister (/usr/bin/nm -B) interface... BSD nm
checking the maximum length of command line arguments... 1572864
checking how to convert x86_64-pc-linux-gnu file names to x86_64-pc-linux-gnu format... func_convert_file_noop
checking how to convert x86_64-pc-linux-gnu file names to toolchain format... func_convert_file_noop
checking for /usr/bin/ld option to reload object files... -r
checking for objdump... objdump
checking how to recognize dependent libraries... pass_all
checking for dlltool... no
checking how to associate runtime and link libraries... printf %s\n
checking for archiver @FILE support... @
checking for strip... strip
checking for ranlib... ranlib
checking command to parse /usr/bin/nm -B output from gcc object... ok
checking for sysroot... no
checking for a working dd... /usr/bin/dd
checking how to truncate binary pipes... /usr/bin/dd bs=4096 count=1
checking for mt... mt
checking if mt is a manifest tool... no
checking for stdio.h... yes
checking for stdlib.h... yes
checking for string.h... yes
checking for inttypes.h... yes
checking for stdint.h... yes
checking for strings.h... yes
checking for sys/stat.h... yes
checking for sys/types.h... yes
checking for unistd.h... yes
checking for sys/time.h... yes
checking for vfork.h... no
checking for dlfcn.h... yes
checking for objdir... .libs
checking if gcc supports -fno-rtti -fno-exceptions... no
checking for gcc option to produce PIC... -fPIC -DPIC
checking if gcc PIC flag -fPIC -DPIC works... yes
checking if gcc static flag -static works... yes
checking if gcc supports -c -o file.o... yes
checking if gcc supports -c -o file.o... (cached) yes
checking whether the gcc linker (/usr/bin/ld -m elf_x86_64) supports shared libraries... yes
checking whether -lc should be explicitly linked in... no
checking dynamic linker characteristics... GNU/Linux ld.so
checking how to hardcode library paths into programs... immediate
checking for shl_load... no
checking for shl_load in -ldld... no
checking for dlopen... yes
checking whether a program can dlopen itself... yes
checking whether a statically linked program can dlopen itself... no
checking whether stripping libraries is possible... yes
checking if libtool supports shared libraries... yes
checking whether to build shared libraries... yes
checking whether to build static libraries... yes
checking how to run the C++ preprocessor... g++ -E
checking for ld used by g++... /usr/bin/ld -m elf_x86_64
checking if the linker (/usr/bin/ld -m elf_x86_64) is GNU ld... yes
checking whether the g++ linker (/usr/bin/ld -m elf_x86_64) supports shared libraries... yes
checking for g++ option to produce PIC... -fPIC -DPIC
checking if g++ PIC flag -fPIC -DPIC works... yes
checking if g++ static flag -static works... yes
checking if g++ supports -c -o file.o... yes
checking if g++ supports -c -o file.o... (cached) yes
checking whether the g++ linker (/usr/bin/ld -m elf_x86_64) supports shared libraries... yes
checking dynamic linker characteristics... (cached) GNU/Linux ld.so
checking how to hardcode library paths into programs... immediate
checking for help2man... no
checking for pdflatex... /usr/bin/pdflatex
checking that pdflatex comes with the necessary packages... yes
checking for pkg-config... pkg-config
checking for library containing xmlTextReaderIsEmptyElement... -lxml2
checking for dlopen in -lc... yes
checking for __gmpz_init in -lgmp... yes
checking for __gmpz_fac_ui in -lgmp... yes
checking for __gmpz_bin_uiui in -lgmp... yes
checking for __gmpz_export in -lgmp... yes
checking for mpfr_init in -lmpfr... yes
checking for mpfr_set_z_2exp in -lmpfr... yes
checking for mpfr_erfc in -lmpfr... yes
checking for mpfi_init in -lmpfi... yes
checking for gzdopen in -lz... yes
checking for libiconv_open in -liconv... no
checking for cos in -lm... yes
checking for xmlTextReaderIsEmptyElement in -lxml2... yes
checking if libgmp is found at runtime... yes
checking if libmpfr is found at runtime... yes
checking if libmpfi is found at runtime... yes
checking if libxml2 is found at runtime... yes
checking for -std=c++11 or -std=gnu++11 support... yes
checking for a suitable installation of fplll... yes
checking if libfplll is found at runtime... yes
checking for -fPIC support... yes
checking for --export-dynamic support... yes
checking for -Xlinker --allow-multiple-definition support... yes
checking for -z muldefs support... yes
checking for support for visibility attributes... no
checking if compiler activates FTZ by default... no
checking if LD -Wl,--version-script works... yes
checking for size_t... yes
checking for working alloca.h... yes
checking for alloca... yes
checking for sys/wait.h that is POSIX.1 compatible... yes
checking for inttypes.h... (cached) yes
checking for stddef.h... yes
checking for stdint.h... (cached) yes
checking for stdlib.h... (cached) yes
checking for string.h... (cached) yes
checking for termios.h... yes
checking for unistd.h... (cached) yes
checking for limits.h... yes
checking for wchar.h... yes
checking for sys/ioctl.h... yes
checking for sys/time.h... (cached) yes
checking for an ANSI C-conforming const... yes
checking for _Bool... yes
checking for stdbool.h that conforms to C99... yes
checking for int8_t... yes
checking for int16_t... yes
checking for int32_t... yes
checking for int64_t... yes
checking for uint8_t... yes
checking for uint16_t... yes
checking for uint32_t... yes
checking for uint64_t... yes
checking for pid_t... yes
checking for size_t... (cached) yes
checking for ssize_t... yes
checking for working volatile... yes
checking for inline... inline
checking for ptrdiff_t... yes
checking for fork... yes
checking for vfork... yes
checking for vprintf... yes
checking for working fork... yes
checking for working vfork... (cached) yes
checking whether gcc needs -traditional... no
checking for GNU libc compatible malloc... yes
checking for GNU libc compatible realloc... yes
checking for gettimeofday... yes
checking for memmove... yes
checking for memset... yes
checking for memcpy... yes
checking for strchr... yes
checking for strerror... yes
checking for strrchr... yes
checking for strtol... yes
checking for dup2... yes
checking for strstr... yes
checking for dladdr... yes
checking for clock_gettime... yes
checking for time... yes
checking for sigaction... yes
checking for sigaddset... yes
checking for sigemptyset... yes
checking for sigprocmask... yes
checking if the system allows %n in a writable segment... no
checking if the Dl_info type is usable... yes
checking if the "__attribute__((fallthrough));" syntax is supported... yes
checking for mp_bitcnt_t... yes
checking that generated files are newer than configure... done
configure: creating ./config.status
config.status: creating Makefile
config.status: creating doc/Makefile
config.status: creating tests-tool/Makefile
config.status: creating tests-lib/Makefile
config.status: creating config.h
config.status: executing depfiles commands
config.status: executing libtool commands
make all-recursive
make[1]: Entering directory '/home/cug/hk324/cml-regression/cakeml-2063/floatingPoint/tools/dandelion/sollya-8.0'
Making all in tests-tool
make[2]: Entering directory '/home/cug/hk324/cml-regression/cakeml-2063/floatingPoint/tools/dandelion/sollya-8.0/tests-tool'
make[2]: Nothing to be done for 'all'.
make[2]: Leaving directory '/home/cug/hk324/cml-regression/cakeml-2063/floatingPoint/tools/dandelion/sollya-8.0/tests-tool'
Making all in tests-lib
make[2]: Entering directory '/home/cug/hk324/cml-regression/cakeml-2063/floatingPoint/tools/dandelion/sollya-8.0/tests-lib'
make[2]: Nothing to be done for 'all'.
make[2]: Leaving directory '/home/cug/hk324/cml-regression/cakeml-2063/floatingPoint/tools/dandelion/sollya-8.0/tests-lib'
make[2]: Entering directory '/home/cug/hk324/cml-regression/cakeml-2063/floatingPoint/tools/dandelion/sollya-8.0'
CC main.o
CC mpfi-compat.lo
CC hash.lo
CC hooks.lo
CC polynomials.lo
CC sollya-library-wrappers.lo
CC sollya-messaging.lo
CC bitfields.lo
CC printf.lo
CC internparser.lo
CC miniparser.lo
CC parser.lo
CC internlexer.lo
CC lexer.lo
CC minilexer.lo
CC assignment.lo
CC autodiff.lo
CC base-functions.lo
CC chain.lo
CC double.lo
CC execute.lo
CC expression.lo
CC external.lo
CC general.lo
CC signalhandling.lo
CC implement.lo
CC implementconst.lo
CC infnorm.lo
CC integral.lo
CC library.lo
CC plot.lo
CC proof.lo
CXX fplll_wrapper.lo
CC fpminimax.lo
CC remez.lo
CC match.lo
CC taylorform.lo
CC chebyshevform.lo
CC chebyshevformaux.lo
CC sollya-help.lo
CC supnorm.lo
CC sturm.lo
CC taylor.lo
CC worstcase.lo
CC xml.lo
CXXLD libsollya.la
CCLD sollya
make[2]: Leaving directory '/home/cug/hk324/cml-regression/cakeml-2063/floatingPoint/tools/dandelion/sollya-8.0'
make[1]: Leaving directory '/home/cug/hk324/cml-regression/cakeml-2063/floatingPoint/tools/dandelion/sollya-8.0'
Scanning [1m$(HOLDIR)/examples/algebra/lib[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/examples/algebra/monoid[0m
Scanning [1m$(HOLDIR)/examples/algebra/group[0m
Scanning [1m$(HOLDIR)/examples/algebra/ring[0m
Scanning [1m$(HOLDIR)/examples/algebra/field[0m
Scanning [1m$(HOLDIR)/examples/algebra/polynomial[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover/Infra[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover/semantics[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover[0m
Scanned 23 directories
Starting work on RealSimpsTheory
Starting work on ResultsTheory
Starting work on sqrtApproxTheory
Starting work on moreRealTheory
ResultsTheory floatingPoint/tools/flover/Infra (8s) OK
Starting work on renameTheory
RealSimpsTheory floatingPoint/tools/flover/Infra (15s) OK
Starting work on MachineTypeTheory
moreRealTheory floatingPoint/tools/dandelion (24s) OK
renameTheory floatingPoint/tools/dandelion (16s) OK
Starting work on realPolyTheory
Starting work on sturmTheory
sqrtApproxTheory floatingPoint/tools/flover (29s) OK
realPolyTheory floatingPoint/tools/dandelion (20s) OK
Starting work on realPolyProofsTheory
Starting work on transcLangTheory
MachineTypeTheory floatingPoint/tools/flover/Infra (34s) OK
Finished $(CAKEMLDIR)/floatingPoint/tools/flover/Infra [#theories: 3] (58.996s)
Starting work on AbbrevsTheory
transcLangTheory floatingPoint/tools/dandelion (19s) OK
Starting work on checkerDefsTheory
AbbrevsTheory floatingPoint/tools/flover/semantics (15s) OK
Starting work on ExpressionsTheory
realPolyProofsTheory floatingPoint/tools/dandelion (20s) OK
Starting work on mcLaurinApproxTheory
sturmTheory floatingPoint/tools/dandelion (48s) OK
Starting work on drangTheory
ExpressionsTheory floatingPoint/tools/flover/semantics (17s) OK
Starting work on FloverMapTheory
checkerDefsTheory floatingPoint/tools/dandelion (16s) OK
Starting work on pointCheckerTheory
FloverMapTheory floatingPoint/tools/flover/semantics (8s) OK
Starting work on ExpressionAbbrevsTheory
drangTheory floatingPoint/tools/dandelion (20s) OK
Starting work on euclidDivTheory
pointCheckerTheory floatingPoint/tools/dandelion (14s) OK
Starting work on transcReflectTheory
ExpressionAbbrevsTheory floatingPoint/tools/flover/semantics (7s) OK
Starting work on ExpressionSemanticsTheory
euclidDivTheory floatingPoint/tools/dandelion (18s) OK
Starting work on sturmComputeTheory
transcReflectTheory floatingPoint/tools/dandelion (17s) OK
Starting work on pointCheckerProofsTheory
ExpressionSemanticsTheory floatingPoint/tools/flover/semantics (21s) OK
Starting work on CommandsTheory
sturmComputeTheory floatingPoint/tools/dandelion (16s) OK
Starting work on floverConnTheory
pointCheckerProofsTheory floatingPoint/tools/dandelion (15s) OK
CommandsTheory floatingPoint/tools/flover/semantics (15s) OK
Finished $(CAKEMLDIR)/floatingPoint/tools/flover/semantics [#theories: 6] (86.241s)
Starting work on EnvironmentsTheory
Starting work on IntervalArithTheory
mcLaurinApproxTheory floatingPoint/tools/dandelion (75s) OK
Starting work on TypeValidatorTheory
floverConnTheory floatingPoint/tools/dandelion (16s) OK
Starting work on ssaPrgsTheory
ssaPrgsTheory floatingPoint/tools/flover (8s) OK
Starting work on approxPolyTheory
EnvironmentsTheory floatingPoint/tools/flover (18s) OK
Starting work on ErrorBoundsTheory
IntervalArithTheory floatingPoint/tools/flover (25s) OK
approxPolyTheory floatingPoint/tools/dandelion (44s) OK
ErrorBoundsTheory floatingPoint/tools/flover (46s) OK
TypeValidatorTheory floatingPoint/tools/flover (67s) OK
Starting work on RealRangeArithTheory
RealRangeArithTheory floatingPoint/tools/flover (7s) OK
Starting work on IntervalValidationTheory
IntervalValidationTheory floatingPoint/tools/flover (29s) OK
Starting work on ErrorValidationTheory
Starting work on transcIntvSemTheory
transcIntvSemTheory floatingPoint/tools/dandelion (24s) OK
ErrorValidationTheory floatingPoint/tools/flover (82s) OK
Finished $(CAKEMLDIR)/floatingPoint/tools/flover [#theories: 9] (316.970s)
Starting work on approxCompErrTheory
approxCompErrTheory floatingPoint/tools/dandelion (24s) OK
Starting work on transcApproxSemTheory
transcApproxSemTheory floatingPoint/tools/dandelion (22s) OK
Starting work on checkerTheory
checkerTheory floatingPoint/tools/dandelion (22s) OK
Starting work on cosDeg3Theory
Starting work on sinDeg3Theory
cosDeg3Theory floatingPoint/tools/dandelion(119s) OK
sinDeg3Theory floatingPoint/tools/dandelion(126s) OK
Don't know how to build necessary target(s): /home/cug/hk324/cml-regression/cakeml-2063/floatingPoint/tools/dandelion/sollya-8.0/readmePrefix