Commit 0cc50396 authored by Heiko Becker's avatar Heiko Becker

Remove not useful stuff from dockerfile and start updating ci script for HOL4

parent 215ffe0f
......@@ -23,23 +23,3 @@ RUN git clone https://github.com/polyml/polyml.git polyml && \
cd polyml && \
git checkout v5.7 && \
./configure && make && make install
ADD ./hol4/.HOLCOMMIT /root/HOLCOMMIT
# RUN cat /root/HOLCOMMIT
# RUN export HOLCOMMIT="$(cat /root/HOLCOMMIT)"
# RUN echo $HOLCOMMIT
# Download HOL4 and compile
RUN git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4 && \
cd HOL4 && \
git checkout `cat /root/HOLCOMMIT` &&\
git rev-parse HEAD &&\
poly < tools/smart-configure.sml && \
./bin/build
RUN echo "HOLDIR=/root/HOL4" >> /root/.profile
ENV HOLDIR /root/HOL4
#!/bin/sh
if [[ $HOLDIR -eq "" ]]
then
#We must be running on ci-server
echo "HOLDIR not set, starting to install HOL4 into ~/ for current user."
echo "If this is not intended, please abort with Ctrl-c"
sleep 5
#Set HOL4 commit variable
HOLCOMMIT="$(cat ./.HOLCOMMIT)"
pushd
cd ~/
git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4
cd HOL4
git checkout $HOLCOMMIT
poly < tools/smart-configure.sml
bin/build
popd
fi
cd ./hol4
#Run configure script to check the versions
./configure_hol.sh
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment