Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions vc-current/.devcontainer/.zshrc
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
autoload -U colors && colors
precmd() {
drawline=""
for i in {1..$COLUMNS}; drawline=" $drawline"
drawline="%U${drawline}%u"
PS1="%F{252}${drawline}
%B%F{124}%n:%~>%b%f "
}

eval $(opam env)

alias ls="ls --color"

58 changes: 58 additions & 0 deletions vc-current/.devcontainer/Dockerfile
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
FROM ubuntu:20.04

## BEGIN: RUNS AS ROOT

# Create a user

ARG USERNAME=cis5000
ARG USER_UID=1000
ARG USER_GID=$USER_UID

RUN apt-get update -y

RUN groupadd --gid $USER_GID $USERNAME \
&& useradd --uid $USER_UID --gid $USER_GID -m $USERNAME --shell /bin/zsh \
#
# [Optional] Add sudo support. Omit if you don't need to install software after connecting.
&& apt-get install -y sudo \
&& echo $USERNAME ALL=\(root\) NOPASSWD:ALL > /etc/sudoers.d/$USERNAME \
&& chmod 0440 /etc/sudoers.d/$USERNAME

## Hack needs root permissions

# See hack.sh
COPY hack.sh /tmp/hack.sh
RUN chmod +x /tmp/hack.sh
RUN /tmp/hack.sh

RUN apt-get install -y build-essential
RUN apt-get install -y linux-libc-dev
RUN apt-get install -y m4
RUN apt-get install -y opam
RUN apt-get install -y time
RUN apt-get install -y zip
RUN apt-get install -y zsh
RUN apt-get install -y libgmp3-dev
RUN DEBIAN_FRONTEND=noninteractive apt-get install -y pkg-config

## Set up user environmnent
COPY .zshrc /home/$USERNAME/


## Run in usermode

# [Optional] Set the default user. Omit if you want to keep the default as root.
USER $USERNAME

# Configure opam/ocaml
RUN opam init -y --disable-sandboxing --compiler=5.3.0
RUN opam switch 5.3.0
RUN opam install -y num
RUN opam repo add -y coq-released https://coq.inria.fr/opam/released
RUN opam pin add -y coq 9.0.0
RUN opam install -y coq-simple-io
RUN opam install -y vscoq-language-server
RUN opam update -y
RUN opam upgrade -y
RUN eval `opam config env`

70 changes: 46 additions & 24 deletions vc-current/.devcontainer/devcontainer.json
Original file line number Diff line number Diff line change
@@ -1,27 +1,49 @@
// For format details, see https://aka.ms/devcontainer.json. For config options, see the
// README at: https://github.com/devcontainers/templates/tree/main/src/ubuntu
{
"image": "bcpierce00/cis5000:8.17.1",
"customizations": {
"vscode": {
"extensions": ["maximedenes.vscoq"],
"settings": {
"coqtop.binPath" : "/home/coq/.opam/default/bin",
"files.exclude": {
"**/*.aux": true,
"**/*.glob": true,
"**/*.vo": true,
"**/*.vos": true,
"**/*.vok": true,
"**/*.html": true,
"**/.*.report": true,
"**/.*.cache": true
},
"coq.loadCoqProject": true,
"coq.coqProjectRoot": ".",
"[coq]": {
"editor.tabSize": 2,
"editor.insertSpaces": true
}
}
"name": "Ubuntu",
// Or use a Dockerfile or Docker Compose file. More info: https://containers.dev/guide/dockerfile
"build": {
"dockerfile": "Dockerfile"
},

// Features to add to the dev container. More info: https://containers.dev/features.
// "features": {},

// Use 'forwardPorts' to make a list of ports inside the container available locally.
// "forwardPorts": [],

// Use 'postCreateCommand' to run commands after the container is created.
// "postCreateCommand": "uname -a",

// Configure tool-specific properties.
"customizations": {
"vscode": {
"extensions": [
"maximedenes.vscoq"
],
"settings": {
"coqtop.binPath" : "/home/cis5000/.opam/4.14.0/bin",
"files.exclude": {
"**/*.aux": true,
"**/*.glob": true,
"**/*.vo": true,
"**/*.vos": true,
"**/*.vok": true,
"**/*.html": true,
"**/.*.report": true,
"**/.*.cache": true
},
"coq.loadCoqProject": true,
"coq.coqProjectRoot": ".",
"[coq]": {
"editor.tabSize": 2,
"editor.insertSpaces": true
}
}
}
}
}

// Uncomment to connect as root instead. More info: https://aka.ms/dev-containers-non-root.
// "remoteUser": "root"
}
17 changes: 17 additions & 0 deletions vc-current/.devcontainer/hack.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
#!/usr/bin/env bash

### HACK - workaround ubuntu libc6 version number bug see: https://forum.odroid.com/viewtopic.php?p=344373

mv /bin/uname /bin/uname.orig
tee -a /bin/uname <<EOF
#!/bin/bash
if [[ \$1 == "-r" ]]; then
echo '4.9.250';
exit
else
uname.orig \$1
fi
EOF

chmod 755 /bin/uname
### END HACK
4 changes: 2 additions & 2 deletions vc-current/Bib.html
Original file line number Diff line number Diff line change
Expand Up @@ -158,12 +158,12 @@ <h1 class="libtitle">Bib<span class="subtitle">Bibliography</span></h1>
</div>
<div class="code">

<span class="comment">(*&nbsp;2024-12-27&nbsp;01:34&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2026-01-06&nbsp;14:19&nbsp;*)</span><br/>
</div>
</div>

<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://rocq-prover.org/">coqdoc</a>
</div>

</div>
Expand Down
2 changes: 1 addition & 1 deletion vc-current/Bib.v
Original file line number Diff line number Diff line change
Expand Up @@ -89,4 +89,4 @@

*)

(* 2024-12-27 01:34 *)
(* 2026-01-06 14:19 *)
Loading