Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

Use CPPFLAGS and LDFLAGS in the C Makefiles and RefC codegen

Open gwerbin opened this issue 3 years ago • 7 comments

I've expanded the scope of this PR since I created the branch, but I don't want to generate extra noise by closing it and renaming the branch to reflect its current purpose. I am happy to do so if the maintainers prefer that.

This PR updates the C source Makefiles and RefC backend compiler to use CPPFLAGS and LDFLAGS in the conventional manner recommended by the GNU Make manual, which should make it easier to build Idris on systems with non-standard installation locations for the GMP library.

This PR also add some missing "phony" declarations which were missing from the Makefiles.


For example, I was unable to build Idris 2 with the Chez backend, because I used MacPorts to install the GMP library into the non-standard prefix of /opt/local/include. Without passing CPPFLAGS, there was no good way to pass the -I/opt/local/include option to the C preprocessor.

Users should now be able to build Idris 2 from scratch with GMP installed anywhere.

For example, a MacPorts on an M1 (ARM) Mac user could follow this recipe if they wanted to use Macports-packaged GMP:

#!/bin/sh

## User configuration

scheme='chez'
chez_prefix="${HOME}/.chezscheme"
idris_prefix="${HOME}/.idris2"

## Set up the system

set -eux

sudo port install pkg-config gmp
mkdir -p ~/src

## Install the Racket Chez fork

git clone --depth 1 https://github.com/racket/ChezScheme ~/src/chezscheme
pushd ~/src/chezscheme
git submodule update --init --recursive

./configure --pb
make tarm64osx.bootquick
mkdir -p "$chez_prefix"
./configure --threads --installschemename='chez' --installprefix="$chez_prefix" 
make -j8
make install

export PATH="${chez_prefix}/bin:${PATH:+:$PATH}"

# Test for success
echo '(+ 83905901 13019309)' | chez -q

popd

## Bootstrap build Idris 2

git clone --depth 1 https://github.com/idris-lang/Idris2 ~/src/idris2
pushd ~/src/idris2

# Bootstrap build
stage1="${PWD}/_boot"  # Must be an absolute path
mkdir -p "$stage1"
make distclean
make bootstrap \
  PREFIX="$stage1" \
  SCHEME="$scheme" \
  CPPFLAGS="$(pkg-config --cflags gmp)" \
  LDFLAGS="$(pkg-config --libs-only-L gmp)"
make install PREFIX="$stage1"

# Final build
stage2="$prefix"
mkdir -p "$stage2"
make clean
make all \
  PREFIX="$stage2" \
  IDRIS2_BOOT="${stage1}/bin/idris2" \
  CPPFLAGS="$(pkg-config --cflags gmp)" \
  LDFLAGS="$(pkg-config --libs-only-L gmp)"
make install PREFIX="$stage2" IDRIS2_BOOT="${stage1}/bin/idris2"
make install-with-src-libs PREFIX="$stage2"
make install-libdocs PREFIX="$stage2"
make install-with-src-api PREFIX="$stage2" IDRIS2_BOOT="${stage2}/bin/idris2"

popd

gwerbin avatar Sep 07 '22 05:09 gwerbin

I think this is something we should support, and the way it's done here lgtm : )

I'd prefer some reassurance from someone more familiar with RefC, but if none comes, the approach with things that look fine and don't have any obvious objections has been "merge, and worst case we can always revert" ^^

OK! I am happy to add a handful of test cases to go along with this. However I'm not sure where to put them, what to name the files, or how to actually make test assertions. There seems to be some naming system in the test suite but I don't see any documentation on how it's supposed to work.

gwerbin avatar Sep 09 '22 02:09 gwerbin

Thanks! I'd still like to add test cases, but I don't know how to structure them, and I don't understand the test file naming convention.

gwerbin avatar Sep 14 '22 20:09 gwerbin

Testing the make parts is probably going to be difficult, since it is so system-dependent.

You could possibly test the functions themselves by exporting them and writing a couple of tests which unset the environment variables, set them to a custom string, tries to get that custom env value using the functions you've defined, and then checks that the two strings match.

In terms of the naming convention: there isn't one defined afaik, but the pattern has been:

  • a sub-directory in the relevant test section (probably refc in this case)
  • with a descriptive name followed by 3 digit numbering (e.g. envflags001)
  • containing:
    • an Idris file importing the relevant modules and containing the test functions
    • a run file which is a shell script which runs the test (see other tests for examples of this)
    • an expected file containing the expected output

Does that help? : )

CodingCellist avatar Sep 15 '22 07:09 CodingCellist

Testing the make parts is probably going to be difficult, since it is so system-dependent.

Indeed, the best (only?) way to test building Idris itself might be in a chroot or container, where I can control where GMP is and isn't installed.

For testing RefC codegen itself, maybe I could create my own library and put the files in ./mylib/{include,lib}, then assert that I can import and use those with %foreign. That should work, right?

You could possibly test the functions themselves by exporting them and writing a couple of tests which unset the environment variables, set them to a custom string, tries to get that custom env value using the functions you've defined, and then checks that the two strings match.

Good idea!

In terms of the naming convention: there isn't one defined afaik, but the pattern has been:

* a sub-directory in the relevant test section (probably `refc` in this case)

* with a descriptive name followed by 3 digit numbering (e.g. `envflags001`)

* containing:
  
  * an Idris file importing the relevant modules and containing the test functions
  * a `run` file which is a shell script which runs the test (see other tests for examples of this)
  * an `expected` file containing the expected output

Does that help? : )

Yes, thank you! I can add this to tests/README.md if that's OK.

gwerbin avatar Sep 15 '22 12:09 gwerbin

I can add this to tests/README.md if that's OK.

I'm sure it is

buzden avatar Sep 16 '22 13:09 buzden

@gwerbin any updates on the tests? I'm happy to help if you're stuck : )

CodingCellist avatar Oct 06 '22 08:10 CodingCellist

Hi @CodingCellist ! Sorry, I've gotten totally bogged down in "real life" things and haven't so much as thought about this. If you feel comfortable with the change as-is, then I don't want to hold it up. I will have to circle back to this at some point.

gwerbin avatar Oct 07 '22 01:10 gwerbin