header.eml

type nav_item =
  | Learn
  | Platform
  | Packages
  | Community
  | Consortium
  | News
  | Playground

let string_of_nav_item = function
  | Learn -> "Learn"
  | Platform -> "Platform"
  | Packages -> "Packages"
  | Community -> "Community"
  | Consortium -> "Consortium"
  | News -> "News"
  | Playground -> "Play"

let url_of_nav_item = function
  | Learn -> Url.learn
  | Platform -> Url.platform
  | Packages -> Url.packages
  | Community -> Url.community
  | Consortium -> Url.consortium
  | News -> Url.changelog
  | Playground -> Url.playground

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
~title
?(_class="")
()
=
  <a href="<%s href %>" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary<%s _class %> <%s if active then "text-primary dark:text-dark-primary underline" else "text-title dark:text-dark-title" %>"><%s title %></a>


let render
?(show_get_started=true)
?(active_top_nav_item: nav_item option)
()
=
let search_dropdown () =
  <div id="header-search-results" aria-live="polite"></div>
  <a class="flex py-2 px-2 mx-2 gap-4 hover:bg-primary_nav_block_hover_10 dark:hover:bg-dark-primary_nav_block_hover_10 font-normal rounded-md text-primary dark:text-dark-primary" href="<%s Url.stdlib %>">
    Standard Library
    <%s! Icons.arrow_top_right_on_square "w-6 h-6" %>
  </a>
in
<header
  class="fixed top-0 z-50 w-full h-20 flex items-center flex-wrap"
  x-data="{ open: false }">  
  <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">
      <% if git_branch <> "main" then (%>
        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>.
      <% ) else ( %>
        ⚠️ Under construction ⚠️ This website will be officialy launched with the first release of Rocq 9.0 in March 2025.
        Until then, there may remain broken links and references to not-yet existing projects.
      <% ); %>
    </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/flowbite@1.5.5/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">
        <a href="<%s Url.index %>" class="block">
          <img src="<%s Rocqproverorg_static.Asset.url "logos/logo-rocq-blue_orange.svg" %>" width="170" alt="Rocq logo" class="dark:hidden">
          <img src="<%s Rocqproverorg_static.Asset.url "logos/logo-rocq-orange_white.svg" %>" width="170" alt="Rocq logo" class="hidden dark:inline">
        </a>
      </li>
    </ul>
    <ul class="order-2 hidden lg:flex items-center">
      <li>
        <form
          <%s! Packages_autocomplete_fragment.form_attributes %>
          action="/packages/search" method="GET">
          <%s! Forms.search_input
            ~name:"q"
            ~label:"Search Rocq packages"
            ~button_attrs:{|type="submit"|}
            ~input_attrs:({|@keydown.stop |} ^ Packages_autocomplete_fragment.input_attributes ~target_sel:"#header-search-results" ~indicator_sel:"#header-search-indicator")
            ~dropdown_html:(search_dropdown ())
            "lg:w-56 xl:w-80"
          %>
        </form>
      </li>
    </ul>
    <ul class="order-1 mr-auto items-center hidden lg:flex font-medium dark:text-white dark:text-opacity-60 dark:font-semibold">
      <% nav_items |> List.iter (fun (n : nav_item) -> %>
      <li><%s! menu_link ~active:(active_top_nav_item=Some n) ~href:(url_of_nav_item n) ~title:(string_of_nav_item n) () %></li>
      <% ); %>
    </ul>
    <% if show_get_started then (%>
    <ul class="order-3 hidden lg:flex items-center">
      <li><a href="<%s Url.getting_started %>" class="border border-secondary dark:border-dark-secondary text-primary dark:text-dark-primary font-bold py-2.5 px-7 whitespace-nowrap rounded">Get Started</a></li>
    </ul>
    <% ); %>
    <ul class="order-1 lg:hidden flex items-center">
      <li
        class="h-12 w-12 hover:bg-tertiary_25 dark:hover:bg-primary_20 flex items-center justify-center rounded-full text-content dark:text-dark-title">
        <button aria-label="open menu" @click="open = ! open">
          <%s! Icons.hamburger_menu "h-8 w-8" %>
        </button>
      </li>
    </ul>
  </nav>

  <div class="bg-black fixed w-full h-full left-0 top-0 opacity-60 z-40" x-show='open' x-cloak></div>

  <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">    
    <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">
            <%s! Icons.close_x "h-8 w-8" %>
          </button>
        </div>
      </li>
      <li class="mt-6 mb-3">
        <form action="/packages/search" method="GET">
          <%s! Forms.search_input
            ~name:"q"
            ~label:"Search Rocq packages"
            ~button_attrs:{|type="submit"|}
            ""
            %>
        </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>
      <% ); %>
      <li>
        <a href="<%s Url.stdlib %>" class="flex py-3 px-1 gap-4 font-semibold text-primary dark:text-dark-primary">Standard Library<%s! Icons.arrow_top_right_on_square "w-6 h-6" %></a>
      </li>
      <li class="mt-3 mb-6">
        <a href="<%s Url.getting_started %>" class="w-full rounded font-normal py-3 px-7 flex items-center justify-center bg-primary dark:bg-dark-primary text-white dark:text-dark-title">Get started</a>
      </li>
      <li>
        <div class="space-x-6 text-2xl flex items-center">
          <a aria-label="Rocq's Zulip" href="https://rocq-prover.zulipchat.com" class="opacity-60 hover:opacity-100 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
            <%s! Icons.zulip "w-6 h-6" %>
          </a>
          <a aria-label="Rocq's Discourse" href="https://coq.discourse.group" class="opacity-60 hover:opacity-100 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
            <%s! Icons.discourse "w-6 h-6" %>
          </a>
          <a aria-label="The Rocq Prover on GitHub" href="https://github.com/coq/coq" class="opacity-60 hover:opacity-100 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
            <%s! Icons.github "w-6 h-6" %>
          </a>
          <a aria-label="The Rocq Prover on Mastodon" rel="me" href="https://mastodon.acm.org/@RocqProver" class="opacity-60 hover:opacity-100 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
            <%s! Icons.mastodon "w-6 h-6" %>
          </a>
        </div>
      </li>
    </ul>
  </nav>
</header>
<%s! Search.script %>