Closed kamweti closed 12 months ago
Thanks for the detailed issue! I'll add the make install-api
command to the base image in a new PR and test if it builds the idris2-python package
Hey @kamweti, merged a PR that should fix it. Can you check that ghcr.io/joshuanianji/idris-2-docker/base:latest
works for you?
looks good, thanks!
closing the issue now.
To Reproduce
base image does
make install
here https://github.com/joshuanianji/idris-2-docker/blob/0cd066eaabfdbe6919f779db3c621ba51c4ab951/base.Dockerfile#L44make install
installs these packageshttps://github.com/idris-lang/Idris2/blob/main/Makefile#L188
building a library such as idris2-python against the base image fails with
the missing dependency is
https://github.com/madman-bob/idris2-python/blob/main/idris2-python.ipkg#L5
this bug can be resolved by installing the api package
Expected behavior
base image should explicitly install
api
package