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
#
# It is tempting to factor this out into multiple Makefiles but that
# makes it less portable, so resist temptation, or move to a more
# sophisticated build system.
#
# 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)
#

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