Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
J
jscoq-light
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package registry
Container registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
GitLab community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Pierre Rousselin
jscoq-light
Commits
572ca93e
Commit
572ca93e
authored
Apr 3, 2020
by
Shachar Itzhaky
Browse files
Options
Downloads
Patches
Plain Diff
[build] Dockerfile for builds.
parent
ccb9b73e
Branches
Branches containing commit
No related tags found
No related merge requests found
Changes
2
Show whitespace changes
Inline
Side-by-side
Showing
2 changed files
etc/docker/Dockerfile
+81
-0
81 additions, 0 deletions
etc/docker/Dockerfile
etc/docker/Makefile
+22
-0
22 additions, 0 deletions
etc/docker/Makefile
with
103 additions
and
0 deletions
etc/docker/Dockerfile
0 → 100644
+
81
−
0
View file @
572ca93e
FROM
debian:10-slim
as
opam
# ------------
# Get OPAM
# ------------
RUN
apt-get update
&&
apt-get
install
--no-install-recommends
-y
\
wget ca-certificates
\
m4 bubblewrap gcc libc6-dev binutils make patch unzip
# We need to install OPAM 2.0 manually for now.
RUN
wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux
-O
/usr/bin/opam
&&
chmod
755 /usr/bin/opam
# Basic OPAM setup
ARG
NJOBS=2
ENV
OPAMJOBS=${NJOBS} \
OPAMROOT=/root/.opamcache \
OPAMROOTISOK=true
RUN
opam init
-a
--bare
--disable-sandboxing
# -----------------
# jsCoq pre-install
# -----------------
RUN
opam switch create jscoq+64bit ocaml-base-compiler.4.07.1
RUN
apt
install
--no-install-recommends
-y
git rsync bzip2 nodejs curl
RUN
curl https://www.npmjs.com/install.sh | sh
# ^ https://github.com/nodejs/help/issues/1877
# ---------------------
# jsCoq toolchain setup
# ---------------------
FROM
opam
as
jscoq-prereq
ARG
REPO=https://github.com/jscoq/jscoq
WORKDIR
/root
RUN
git clone
--recursive
${
REPO
}
WORKDIR
jscoq
RUN
./etc/toolchain-setup.sh
--64
RUN
opam clean
-a
-c
# -----------
# jsCoq build
# -----------
FROM
jscoq-prereq
as
jscoq
ARG
NJOBS=4
RUN
git pull
RUN
eval
$(
opam
env
)
&&
make coq
&&
make jscoq
# - addons
RUN
eval
$(
opam
env
)
&&
make addons
ADDONS
=
"mathcomp"
RUN
eval
$(
opam
env
)
&&
opam
install
-y
elpi.1.8.0
&&
make addons
ADDONS
=
"elpi"
RUN
eval
$(
opam
env
)
&&
make addons
ADDONS
=
"equations"
# - remake packages after addon build
# (also creates `*.cma.js`)
RUN
eval
$(
opam
env
)
&&
rm
-rf
_build/jscoq+64bit/coq-pkgs
\
&&
make jscoq
ADDONS
=
"mathcomp elpi equations"
# - dist tarballs
RUN
eval
$(
opam
env
)
&&
make dist-tarball
&&
make dist-npm
\
&&
mkdir
dist
&&
mv
_build/dist/
*
.tar.gz dist
# jsCoq SDK
#RUN cp -rL _build/install/jscoq+64bit/ ./dist && \
# rm dist/bin/*.byte dist/bin/*.opt \
# dist/lib/coq/*/*.cmxs \
# `find dist -regex '.*\.\(cm\(a\|t\|ti\)\|mli?\)'`
#FROM debian:10-slim
#COPY --from=0 /root/jscoq/dist /opt/jscoq
This diff is collapsed.
Click to expand it.
etc/docker/Makefile
0 → 100644
+
22
−
0
View file @
572ca93e
.PHONY
:
build dist serve
WHO
=
jscoq
export
REPO
=
https://github.com/
$(
WHO
)
/jscoq
export
NJOBS
?=
4
ARGS
=
--build-arg
REPO
--build-arg
NJOBS
build
:
docker build
.
--target
opam
$(
ARGS
)
-t
opam
docker build
.
--target
jscoq-prereq
$(
ARGS
)
-t
jscoq:prereq
docker build
.
--target
jscoq
$(
ARGS
)
-t
jscoq
dist
:
docker run
--name
jscoq-get-dist jscoq
docker
cp
jscoq-get-dist:/root/jscoq/dist .
docker
rm
jscoq-get-dist
serve
:
docker run
--publish
8080:8080
--rm
-it
jscoq
\
bash
-c
"npx http-server _build/dist"
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
sign in
to comment