Skip to content
Merged
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
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ jobs:
run: opam exec -- dune build @install

- name: Run tests
run: opam exec -- dune test
run: opam exec -- make test

# - name: Format code
# run: opam exec -- dune build --auto-promote @fmt
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/debug-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ jobs:
run: opam exec -- dune build @install

- name: Run tests
run: opam exec -- dune test
run: opam exec -- make test

- name: Format code
run: opam exec -- dune build --auto-promote @fmt
Expand Down
11 changes: 11 additions & 0 deletions Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,17 @@ WORKDIR /home/opam
ADD rocqproverorg.opam rocqproverorg.opam
RUN opam install . --deps-only

# Git commit and branch information
ARG GIT_COMMIT
RUN echo "Based on commit: $GIT_COMMIT"
ENV GIT_COMMIT=${GIT_COMMIT}
LABEL rocqproverorg=${GIT_COMMIT}

ARG GIT_BRANCH
RUN echo "Based on branch: $GIT_BRANCH"
ENV GIT_BRANCH=${GIT_BRANCH}
LABEL rocqproverorg_branch=${GIT_BRANCH}

# Build project
COPY --chown=opam:opam . .
RUN opam exec -- dune build @install --profile=release
Expand All @@ -37,6 +43,11 @@ RUN echo "Based on commit: $GIT_COMMIT"
ENV GIT_COMMIT=${GIT_COMMIT}
LABEL rocqproverorg=${GIT_COMMIT}

ARG GIT_BRANCH
RUN echo "Based on branch: $GIT_BRANCH"
ENV GIT_BRANCH=${GIT_BRANCH}
LABEL rocqproverorg_branch=${GIT_BRANCH}

RUN apk update && apk add --update libev gmp git

RUN chmod -R 755 /var
Expand Down
16 changes: 11 additions & 5 deletions Makefile
Original file line number Diff line number Diff line change
@@ -1,7 +1,12 @@
.DEFAULT_GOAL := all
DOC_PATH=`pwd`/rocq-doc/
GIT_HEAD=`git rev-parse HEAD`
GIT_COMMIT=${GIT_HEAD}`git diff --quiet HEAD || echo "-dirty"`
DOC_PATH=$(shell pwd)/rocq-doc/
GIT_HEAD=$(shell git rev-parse HEAD)
GIT_DIRTY=$(shell git diff --quiet HEAD || echo "-dirty")
GIT_COMMIT=${GIT_HEAD}${GIT_DIRTY}
GIT_BRANCH=$(shell git branch --show-current)

export GIT_COMMIT
export GIT_BRANCH

.PHONY: all
all:
Expand All @@ -11,6 +16,7 @@ all:
show-config:
@echo "DOC_PATH="${DOC_PATH}
@echo "GIT_COMMIT="${GIT_COMMIT}
@echo "GIT_BRANCH="${GIT_BRANCH}

.PHONY: deps
deps: create_switch ## Install development dependencies
Expand Down Expand Up @@ -72,7 +78,7 @@ fmt: ## Format the codebase with ocamlformat

.PHONY: watch
watch: update-local-doc ## Watch for the filesystem and rebuild on every change
DOC_PATH=${DOC_PATH} GIT_COMMIT=${GIT_COMMIT} opam exec -- dune build @run -w --force --no-buffer
opam exec -- dune build @run -w --force --no-buffer

.PHONY: utop
utop: ## Run a REPL and link with the project's libraries
Expand All @@ -85,7 +91,7 @@ scrape: ## Generate the po files

.PHONY: docker
docker: ## Generate docker container
docker build --build-arg GIT_COMMIT=`git rev-parse HEAD` -f Dockerfile . -t rocqproverorg:latest
docker build --build-arg GIT_COMMIT=${GIT_COMMIT} --build-arg GIT_BRANCH=${GIT_BRANCH} -f Dockerfile . -t rocqproverorg:latest

.PHONY: linkcheck
linkcheck:
Expand Down
1 change: 1 addition & 0 deletions compose.yml
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ services:
context: .
args:
- GIT_COMMIT=${GIT_COMMIT}
- GIT_BRANCH=${GIT_BRANCH}
ports:
- "127.0.0.1:${LOCAL_PORT}:8080"
volumes:
Expand Down
10 changes: 7 additions & 3 deletions src/rocqproverorg_frontend/components/footer.eml
Original file line number Diff line number Diff line change
Expand Up @@ -173,9 +173,13 @@ let primary_footer () =
<div class="flex w-full md:hidden">
<%s! LightDarkModeSwitch.render %>
</div>
<div class="flex mt-6 space-y-4">
<% let commit = try Sys.getenv "GIT_COMMIT" with Not_found -> failwith "Environment variable GIT_COMMIT is not set" in %>
<%s! link ~href:("https://github.com/coq/rocq-prover.org/commit/" ^ commit) ~name:"GitHub Source" %>
<div class="flex mt-6 space-y-4 hidden">
<% let commit = try Sys.getenv "GIT_COMMIT" with Not_found -> failwith "Environment variable GIT_COMMIT is not set" in
let branch = try Sys.getenv "GIT_BRANCH" with Not_found -> failwith "Environment variable GIT_BRANCH is not set" in %>
<div class="text-base leading-6 text-content dark:text-dark-title">
GitHub <a href="https://github.com/coq/rocq-prover.org/tree/<%s branch %>" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">branch</a>
and <a href="https://github.com/coq/rocq-prover.org/commit/<%s commit %>">commit</a>.
</div>
<% ; %>
</div>
</div>
Expand Down
31 changes: 26 additions & 5 deletions src/rocqproverorg_frontend/components/header.eml
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,10 @@ let url_of_nav_item = function

let nav_items = [ Learn; Platform; Packages; Community; Consortium; News; Playground ]

let git_branch = try Sys.getenv "GIT_BRANCH" with Not_found -> failwith "Environment variable GIT_BRANCH is not set"
let git_commit = try Sys.getenv "GIT_COMMIT" with Not_found -> failwith "Environment variable GIT_COMMIT is not set"
let git_short_commit = if String.length git_commit > 6 then String.sub git_commit 0 7 else git_commit

let menu_link
~(active: bool)
~href
Expand All @@ -50,8 +54,27 @@ let search_dropdown () =
</a>
in
<header
class="fixed top-0 z-50 w-full h-20 flex items-center "
x-data="{ open: false }">
class="fixed top-0 z-50 w-full h-20 flex items-center flex-wrap"
x-data="{ open: false }">
<% if git_branch <> "main" then (%>
<div id="alert-border-2" class="bg-primary_25 border-secondary border-t-4 bottom-0 dark:bg-dark-card fixed flex items-center justify-center p-4 text-center tracking-wide w-full" role="alert">
<svg class="flex-shrink-0 w-4 h-4" aria-hidden="true" xmlns="http://www.w3.org/2000/svg" fill="currentColor" viewBox="0 0 20 20">
<path d="M10 .5a9.5 9.5 0 1 0 9.5 9.5A9.51 9.51 0 0 0 10 .5ZM9.5 4a1.5 1.5 0 1 1 0 3 1.5 1.5 0 0 1 0-3ZM12 15H8a1 1 0 0 1 0-2h1v-3H8a1 1 0 0 1 0-2h2a1 1 0 0 1 1 1v4h1a1 1 0 0 1 0 2Z"/>
</svg>
<div class="ms-3 text-sm font-medium">
You are viewing the <a class="font-semibold underline hover:no-underline" href="https://github.com/coq/rocq-prover.org/tree/<%s git_branch %>"><%s git_branch %> branch</a> of the website @
<a class="font-semibold underline hover:no-underline" href="https://github.com/coq/rocq-prover.org/commit/<%s git_commit %>"><%s git_short_commit %></a>,
not the <a class="font-semibold underline hover:no-underline" href="https://rocq-prover.org">live version</a>.
</div>
<button type="button" class="ms-3 -mx-1.5 -my-1.5 bg-red-50 text-red-500 rounded-lg focus:ring-2 focus:ring-red-400 p-1.5 hover:bg-red-200 inline-flex items-center justify-center h-8 w-8 dark:bg-gray-800 dark:text-red-400 dark:hover:bg-gray-700" data-dismiss-target="#alert-border-2" aria-label="Close">
<span class="sr-only">Dismiss</span>
<svg class="w-3 h-3" aria-hidden="true" xmlns="http://www.w3.org/2000/svg" fill="none" viewBox="0 0 14 14">
<path stroke="currentColor" stroke-linecap="round" stroke-linejoin="round" stroke-width="2" d="m1 1 6 6m0 0 6 6M7 7l6-6M7 7l-6 6"/>
</svg>
</button>
</div>
<script src="https://unpkg.com/[email protected]/dist/flowbite.js"></script>
<% ); %>
<nav class="bg-background container-fluid dark:bg-dark-background_navigation flex gap-5 h-20 header items-center justify-between rounded-b-lg shadow-sm wide xl:gap-8">
<ul class="order-0 space space-x-5 xl:space-x-8 items-center flex text-content font-medium dark:text-title dark:text-opacity-60 dark:font-semibold">
<li style="width:170px">
Expand Down Expand Up @@ -102,14 +125,13 @@ in
<nav class="z-50 h-full fixed right-0 top-0 max-w-full w-96 bg-background dark:bg-dark-background shadow-lg" x-show="open" x-cloak
@click.away="open = false" x-transition:enter="transition duration-200 ease-out"
x-transition:enter-start="translate-x-full" x-transition:leave="transition duration-100 ease-in"
x-transition:leave-end="translate-x-full">
x-transition:leave-end="translate-x-full">
<ul class="text-content p-6 font-semibold">
<li class="flex justify-between items-center">
<a href="<%s Url.index %>">
<img src="<%s Rocqproverorg_static.Asset.url "logos/logo-rocq-blue_orange.svg" %>" width="132" alt="Rocq logo" class="dark:hidden">
<img src="<%s Rocqproverorg_static.Asset.url "logos/logo-rocq-white.svg" %>" width="132" alt="Rocq logo" class="hidden dark:inline">
</a>

<div class=""
x-on:click="open = false">
<button aria-label="close" class="text-content dark:text-dark-title">
Expand All @@ -127,7 +149,6 @@ in
%>
</form>
</li>

<% nav_items |> List.iter (fun (n : nav_item) -> %>
<li><%s! menu_link ~_class:"block" ~active:(active_top_nav_item=Some n) ~href:(url_of_nav_item n) ~title:(string_of_nav_item n) () %></li>
<% ); %>
Expand Down
Loading