Way to move the libraries out of /root

[xhalo32]

Hi 👋 ,

Thanks for your excellent work!

I am looking for a way to move the libraries out of /root, but constantly run into the following error when launching idris:

Uncaught error: Error: Module Prelude not found

Do you know if recompiling is necessary or I'm just missing some environment configuration?

In the meanwhile I just change owner of the /root directory in my container: https://gitlab.com/niklashh/idris2-toolbox

[joshuanianji]

Hey @xhalo32, thanks for checking out my project!

I'd love to know more about your project: I don't recompile anything when I move libraries out of /root when I make my ubuntu, debian, and devcontainer images, and your container files in the linked repository look like they should work.

I tried to run it locally but couldn't find a way to get toolbox to work on mac, do you have any tips? It looks like it's a linux-specific package, and I couldn't get it to install correctly inside docker containers either.

---

In the meantime, here's an example of a Debian image copying Idris2. It works for me, but let me know if there are any errors on your end! We can debug from there.

ARG IDRIS_VERSION=latest

FROM ghcr.io/joshuanianji/idris-2-docker/base:${IDRIS_VERSION} as base

FROM debian:latest

# add idris2 and scheme from builder
COPY --from=base /root/.idris2 /root/.idris2
COPY --from=base /usr/bin/scheme /usr/bin/scheme
# copy csv9.5* to /usr/lib
COPY --from=base /root/scheme-lib/ /usr/lib/

ENV PATH="/root/.idris2/bin:${PATH}"

RUN apt-get update \
    && apt-get -y install rlwrap \
    && apt-get clean 

# This command won't output anything when you build with buildkit
RUN idris2 --version

Build and run it:

docker build -t idris-test --no-cache .
docker run -it idris-test idris2 --version

[xhalo32]

Hi, thanks for your reply!

What I meant with moving out of /root, is to move the libraries somewhere like /usr/local/lib, to avoid having to change the ownership of /root when using the container as a non-root user. Like with this COPY directive

COPY --from=base /root/.idris2 /usr/local/lib/idris2

You are probably not familiar with the toolbox project, which is the system I am using to run this container with. It uses podman rather than docker to manage the images and containers. I don't know whether it works on OSX or not (I'm on Fedora).

[joshuanianji]

Hi, thanks for clarifying! I personally haven't tried what you're doing right now, but I remember I had the same errors when the Idris lib files weren't copied properly.

I'm out of the house so I can't try this right now, but maybe setting the LD_LIBRARY_PATH to /usr/local/lib/idris2/lib will make the Idris2 binaries able to find the Prelude lib.

Let me know if it works!

[joshuanianji]

Okay, came home and tested out the Dockerfile below, it seems to work! Let me know if this is something you're looking for.

ARG IDRIS_VERSION=latest

FROM ghcr.io/joshuanianji/idris-2-docker/base:${IDRIS_VERSION} as base

FROM debian:latest

# add idris2 and scheme from builder
COPY --from=base /root/.idris2 /usr/local/lib/idris2
COPY --from=base /usr/bin/scheme /usr/bin/scheme
# copy csv9.5* to /usr/lib
COPY --from=base /root/scheme-lib/ /usr/lib/

ENV PATH="/usr/local/lib/idris2/bin:${PATH}"
ENV LD_LIBRARY_PATH="/usr/local/lib/idris2/lib:${LD_LIBRARY_PATH}"

RUN apt-get update \
    && apt-get -y install rlwrap \
    && apt-get clean 

# This command won't output anything when you build with buildkit
RUN idris2 --version

Running it:

$ docker build -t idris-test --no-cache .
$ docker run -it idris-test idris2 --version
Idris 2, version 0.5.1-188de8b4c
$ docker run -it idris-test which idris2
/usr/local/lib/idris2/bin/idris2

[xhalo32]

Thanks for your help, however the same error persists:

Welcome to Idris 2.  Enjoy yourself!
Uncaught error: Error: Module Prelude not found

idris2 --version works without it finding the prelude, but if you open the repl by running idris2 you get the previous error message.

I am 90% certain you need to recompile idris2 to fix this

[joshuanianji]

Hey @xhalo32, so sorry for the late response! School got super busy but I just finished midterms, so I've finally had some time to work on this project again.

It turns out rebuilding is indeed the right approach. I can rebuild using an existing Idris installation from the base image and set the PREFIX argument to /usr/local/lib/idris2.

Here is the full Dockerfile below:

ARG IDRIS_VERSION=latest

FROM ghcr.io/joshuanianji/idris-2-docker/base:${IDRIS_VERSION} as base

WORKDIR /build
RUN git clone https://github.com/idris-lang/Idris2.git
WORKDIR /build/Idris2
RUN make all PREFIX=/usr/local/lib/idris2
RUN make install PREFIX=/usr/local/lib/idris2

FROM debian:latest 

# add idris2 and scheme from base
COPY --from=base /usr/local/lib/idris2 /usr/local/lib/idris2
COPY --from=base /usr/bin/scheme /usr/bin/scheme
# copy csv9.5* to /usr/lib
COPY --from=base /root/scheme-lib/ /usr/lib/

# set new Idris2
ENV PATH="/usr/local/lib/idris2/bin:${PATH}"
ENV LD_LIBRARY_PATH="/usr/local/lib/idris2/lib:${LD_LIBRARY_PATH}"

And after building it, here's what I get: