Merge pull request #62 from coq/staging

Staging branch support

Author: mattam82

.github/workflows/ci.yml

@@ -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

.github/workflows/debug-ci.yml

@@ -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

Dockerfile

@@ -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
@@ -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

Makefile

@@ -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:
@@ -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
@@ -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
@@ -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:

compose.yml

@@ -5,6 +5,7 @@ services:
       context: .
       args:
         - GIT_COMMIT=${GIT_COMMIT}
+        - GIT_BRANCH=${GIT_BRANCH}
     ports:
       - "127.0.0.1:${LOCAL_PORT}:8080"
     volumes:

src/rocqproverorg_frontend/components/footer.eml

@@ -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>

src/rocqproverorg_frontend/components/header.eml

@@ -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
@@ -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">
@@ -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">
@@ -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>
       <% ); %>