katrinafyi

Background:

• Using --base-url and --root-dir together is surprising. The root-dir (which is a filesystem path) gets prefixed onto the base URL (which is a URL). This happens to build a valid URL on Unix, but it will almost always be a broken link. On Windows, it will put C:\ inside the URL which is surely wrong. Discussed in lycheeverse/lychee#1912 (comment)
• Using --base-url with local files can be surprising, because the local folder structure is not considered when making the URLs - the local folder path is dropped entirely. lycheeverse/lychee#1296 was a similar issue (now fixed) for remote URLs. This problem is similar but for local URLs instead.
• Using --root-dir surprisingly (and negatively) affects / links in remote HTML files lycheeverse/lychee#1964

Proposal:

Questions:

• How to communicate this change to users? Should the current behaviour be kept accessible?

katrinafyi

(* AUTO-GENERATED LIFTER FILE *)

open Offline_utils

let f_aarch64_float_arithmetic_max_min v_enc v_pc : unit = 
  begin
    let v_result__1_copyprop = ref (undefined ()) in
    let v_Exp13__2 = f_decl_bv ("Exp13__2") (Z.of_string "32") in
    let v_Exp15__2 = f_decl_bv ("Exp15__2") (Z.of_string "32") in
    let v_Exp17__2 = f_decl_bv ("Exp17__2") (Z.of_string "32") in

katrinafyi

diff --git a/mill-derivation/lib/dependencies.nix b/mill-derivation/lib/dependencies.nix
index 422dacb..346ecea 100644
--- a/mill-derivation/lib/dependencies.nix
+++ b/mill-derivation/lib/dependencies.nix
@@ -6,7 +6,9 @@
   gnused,
   lib,
   rdfind,
-  sbt,
+  mill,

katrinafyi

#!/usr/bin/env python3
# vim: ts=2 sts=2 et sw=2

from collections import defaultdict
import os
import re
import sys
import json

'''

katrinafyi

#include <stdio.h>
int main(void){return 3;}

katrinafyi

Tue, Oct 29, 2024, 16:26:26 - kait: hello, i need a slightly customised LLVM for my work and the llvmPackages Nix code is a bit confusing. what are the suggested ways to override LLVM with cmake flags (e.g. LLVM\_TARGETS\_TO\_BUILD) and to point it to a particular commit of the llvm repo (i.e. override the src)?
Tue, Oct 29, 2024, 16:27:53 - kait: i would like to do this in the "correct" way to get a consistent llvmPackages
Tue, Oct 29, 2024, 16:29:46 - ElvishJerricco: kait: IIRC the llvm nix code is pretty complicated, and I doubt it's designed with that use case in mind (Tristan Ross or emily can probably correct me if I'm wrong on that). It might be easiest to start with editing the expressions in nixpkgs directly to get started
Tue, Oct 29, 2024, 16:30:41 - emily: I think it does actually let you add new versions
Tue, Oct 29, 2024, 16:30:56 - emily: if you look at `llvmVersions` and how it's used in `pkgs/development/compilers/llvm/default.nix `
Tue, Oct 29, 2024, 16:30:58 - ElvishJerricco: oh, that must 

katrinafyi

var coqdocjs = coqdocjs || {};

coqdocjs.repl = {
    " ": "\u00A0",
    "forall": "∀",
    "exists": "∃",
    "~": "¬",
    "/\\": "∧",
    "\\/": "∨",
    "->": "→",

katrinafyi

#!/usr/bin/env python3
# vim: ts=2:sw=2:expandtab:autoindent

"""
format_anything.py implements pretty-printing of any expression
with parentheses.
"""

import io
import re

katrinafyi

From 1c0d426700fe52da7e46bc17a111e103ded0f91b Mon Sep 17 00:00:00 2001
From: rina <k@rina.fyi>
Date: Mon, 15 Jul 2024 16:32:32 +1000
Subject: [PATCH] ci: discover histogram parts dynamically

untested
---
 .github/workflows/run-examples.yml | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

katrinafyi

theory Scratch
  imports CTT.CTT
begin

lemma
  assumes "X type" "⋀x. x:X ⟹ P(x) type" "Q type"
  assumes "g : ∑x:X. (P(x) ⟶ Q)"  
  shows "h : (∏x:X. P(x)) ⟶ Q"
  using assms
  sorry