W95Psp

Tutorial: https://hacspec.org/book/tutorial/index.html Docker instructions: https://github.com/hacspec/hax/tree/franziskus/toronto-2024/examples#extracting-f-code

W95Psp

# This is a generically useful Makefile for F* that is self-contained
#
# We expect:
#  1. `fstar.exe` to be in PATH (alternatively, you can also set
#     $FSTAR_HOME to be set to your F* repo/install directory)
#
#  2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH.
#
#  3. the extracted Cargo crate to have "hax-lib" as a dependency:
#     `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}`

W95Psp

module DeBruijn

open FStar.Tactics

// Let [abs] a term that consists in nested abstractions. Note [fun x y z -> ...] is syntactic sugar for [fun x -> fun y -> fun z -> ...]
let abs = (`(fun x -> fun y -> fun z -> (x, y, z)))

let get_let_bv_index (tv: term_view): string
  = match tv with
  | Tv_Let _ _ bv _ _ -> string_of_int (inspect_bv bv).bv_index

W95Psp

let formatTime = time => ('00:00:00,00'.substr(0, 11-time.length) + time.replace(/\./g, ',')) + '0'
$$('.subtitle-element-container').map(x => [x.querySelector('textarea.subtitle-element-textarea').value, [...x.querySelectorAll('input.subtitle-element-bounds-input')].map(x => x.value).map(formatTime)])
   .map(([text, times]) => ({text, times})).map(({text, times}, i) => `${i+1}
${times[0]} --> ${times[1]}
${text}`).join('\n\n')

W95Psp

inotifywait -r -m -e modify default.nix | \
  while read x; do (
    nix-build 2>&1 | tee >(
      grep -Po "File .\K.*(?=.sty' not found)" | \
        tee >(tr -d '\n' | xsel -i -b)
    )
  ); done