Skip to content

Allow passing custom library prefix #2

@mseri

Description

@mseri

Flint fails to compile for me with

- File "flint/flint/dune", line 5, characters 0-9578:
-   5 | (rule
-   6 |  (alias flint2_build)
-   7 |  (targets
- .....
- 271 |     (copy prefix/include/flint/thread_pool.h thread_pool.h)
- 272 |     (copy prefix/include/flint/thread_support.h thread_support.h)
- 273 |     (copy prefix/include/flint/ulong_extras.h ulong_extras.h)))))
- (cd _build/.sandbox/a98ebd6af55d85543f7c87e281f980d4/default/flint/flint/flint2 && ./configure --prefix=../prefix 'CFLAGS=-fPIC -D_GNU_SOURCE')
- Invalid GMP directory
[ERROR] The compilation of flint.0.1.5 failed at "dune build -p flint -j 7 @install".

This is because flint looks by default into /usr/local. On my system (macos M1 and x86_64 with macports) I need to call configure as ./configure --with-gmp=/opt/local --with-mpfr=/opt/local --with-blas=/opt/local/include/lapack to make flint configure.

I still get some weird failures on ARM after that change:

(cd _build/.sandbox/8d3842cec7d00cf7bfbddd396f2cb247/default/flint/flint/flint2 && ./configure --prefix=../prefix 'CFLAGS=-fPIC -D_GNU_SOURCE' --with-gmp=/opt/local --with-mpfr=/opt/local --with-blas=/opt/local)
./configure: line 125: config.log: Permission denied
./configure: line 126: config.log: Permission denied
cp: fmpz/fmpz.c: Permission denied
cp: fmpz-conversions.h: Permission denied
Configuring...unknown-Darwin
./configure: line 475: config.log: Permission denied
cp: fft_tuning.h: Permission denied
Testing __builtin_popcountl..../configure: line 574: config.log: Permission denied
./configure: line 581: build/test-popcnt.c: Permission denied
yes
./configure: line 585: config.log: Permission denied
Testing __thread..../configure: line 662: config.log: Permission denied
yes
Testing fenv..../configure: line 691: config.log: Permission denied
yes
./configure: line 698: config.log: Permission denied
Testing big endian..../configure: line 711: config.log: Permission denied
no
./configure: line 717: config.log: Permission denied
Testing cpu_set_t..../configure: line 736: config.log: Permission denied
no
./configure: line 749: config.log: Permission denied
./configure: line 798: flint-config.h: Permission denied
./configure: line 799: flint-config.h: Permission denied
./configure: line 800: flint-config.h: Permission denied
./configure: line 801: flint-config.h: Permission denied
./configure: line 802: flint-config.h: Permission denied
./configure: line 803: flint-config.h: Permission denied
./configure: line 804: flint-config.h: Permission denied
./configure: line 805: flint-config.h: Permission denied
./configure: line 806: flint-config.h: Permission denied
./configure: line 807: flint-config.h: Permission denied
./configure: line 808: flint-config.h: Permission denied
./configure: line 816: flint-config.h: Permission denied
./configure: line 821: Makefile: Permission denied
./configure: line 822: Makefile: Permission denied
./configure: line 823: Makefile: Permission denied
./configure: line 824: Makefile: Permission denied
./configure: line 825: Makefile: Permission denied
./configure: line 826: Makefile: Permission denied
./configure: line 827: Makefile: Permission denied
./configure: line 828: Makefile: Permission denied
./configure: line 829: Makefile: Permission denied
./configure: line 830: Makefile: Permission denied
./configure: line 831: Makefile: Permission denied
./configure: line 832: Makefile: Permission denied
./configure: line 833: Makefile: Permission denied
./configure: line 834: Makefile: Permission denied
./configure: line 835: Makefile: Permission denied
./configure: line 836: Makefile: Permission denied
./configure: line 837: Makefile: Permission denied
./configure: line 838: Makefile: Permission denied
./configure: line 839: Makefile: Permission denied
./configure: line 840: Makefile: Permission denied
./configure: line 841: Makefile: Permission denied
./configure: line 842: Makefile: Permission denied
./configure: line 843: Makefile: Permission denied
./configure: line 844: Makefile: Permission denied
./configure: line 845: Makefile: Permission denied
./configure: line 846: Makefile: Permission denied
./configure: line 847: Makefile: Permission denied
./configure: line 848: Makefile: Permission denied
./configure: line 849: Makefile: Permission denied
./configure: line 850: Makefile: Permission denied
./configure: line 851: Makefile: Permission denied
./configure: line 852: Makefile: Permission denied
./configure: line 853: Makefile: Permission denied
./configure: line 854: Makefile: Permission denied
./configure: line 855: Makefile: Permission denied
./configure: line 856: Makefile: Permission denied
./configure: line 857: Makefile: Permission denied
./configure: line 858: Makefile: Permission denied
./configure: line 859: Makefile: Permission denied
./configure: line 861: Makefile: Permission denied
FLINT was successfully configured.
./configure: line 864: config.log: Permission denied

Do you by chance know why these happen? If I enter the flint2 folder and configure and compile by hand it works fine.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions