jimwhite’s gists

jimwhite / make -j 1.log

Last active January 7, 2026 16:40

Make books error log

	[internal] load build definition from Dockerfile
	transferring 6279/0 0.004
	[internal] load metadata for quay.io/jupyter/minimal-notebook:latest
	[internal] load .dockerignore
	[ 1/18] FROM quay.io/jupyter/minimal-notebook:latest@sha256:182e233fa335cb7b92d6c5ac2222cf7036b1848ba317b746c4708e47a390661e
	resolve quay.io/jupyter/minimal-notebook:latest@sha256:182e233fa335cb7b92d6c5ac2222cf7036b1848ba317b746c4708e47a390661e 0/0 0.008
	[internal] load build context
	transferring 22020/0 0.012
	[ 3/18] RUN apt-get update && apt-get install -y --no-install-recommends build-essential gcc git automake autoconf make libcurl4-openssl-dev ca-certificates libssl-dev wget perl zlib1g-dev libzstd-dev libczmq-dev curl unzip nodejs npm pipx rlwrap retry sbcl && rm -rf /var/lib/apt/lists/* # remove cached apt files
	[ 6/18] COPY archlinux-cl/asdf-add /usr/loca

jimwhite / proteins.lisp

Last active August 16, 2025 19:18

Small ACL2 Fixed Types (FTY) example by Perplexity - https://www.perplexity.ai/search/are-there-any-examples-of-usin-sUkfi5iAQbulULPiwizXOw?7=r

	(include-book "centaur/fty/top" :dir :system)
	;;; https://github.com/acl2/acl2/tree/master/books/centaur/fty
	;;; FTY introduced in Fix Your Types by Swords & Davis at 2015 ACL2 workshop - https://arxiv.org/abs/1509.06079
	;;; A bigger type book which includes FTY: https://github.com/acl2/acl2/tree/master/books/coi/types

	(fty::defprod protein
	((name stringp)
	(description stringp)
	(source symbolp) ;; e.g., 'milk, 'plant
	(dose natp))

jimwhite / claude-4-chat.md

Last active August 13, 2025 17:39

<|channel|>analysis<|message|>Need to provide example code using ACL2 (a theorem prover) to generate Dockerfile with constraints verified. Explain approach, snippets.<|end|>

Specify the properties you want a Docker image (and the container that runs from it) to satisfy.
Prove—inside ACL2—that a concrete Dockerfile meets those properties.
Export the verified Dockerfile as plain text, ready to be built with docker build.

The example is deliberately small so you can run it on a laptop, but the same ideas scale to much larger images (e.g., multi‑stage builds, custom entrypoints, network policies, etc.).

jimwhite / qwen-3-30b-chat.md

Last active August 13, 2025 17:40

qwen-coder-30b: write an example of using ACL2 to generate a Dockerfile with verified constraints on how the Dockerfile and the container its image creates can operate

Here's an example of using ACL2 to generate a Dockerfile with verified constraints on container operations:

(include-book "std/lists/append" :dir :system)
(include-book "std/lists/nth" :dir :system)
(include-book "std/strings/str" :dir :system)
(include-book "std/strings/char" :dir :system)

;; Define a structure for Dockerfile constraints
(defstruct dockerfile-constraint

jimwhite / openhands.sh

Created November 6, 2024 01:54

Run OpenHands on Ubuntu

	# My version of https://docs.all-hands.dev/modules/usage/installation

	# On MacOS
	DOCKER="docker"
	# or for Ubuntu
	DOCKER="sudo docker"

	# 0.12.3 (2024-10-04) didn't work for me - litellm failed but 0.12.2 does.
	VERSION="0.12.2"
	SANDBOX_RUNTIME_CONTAINER_IMAGE="docker.all-hands.dev/all-hands-ai/runtime:$VERSION-nikolaik"

jimwhite / gist:93c91457d503c2a541b709c63bb8f8cd

Last active July 6, 2024 02:40

try.ocamlpro.com of TAPL https://github.com/roehst/tapl-implementations/blob/master/fomsub/syntax.ml

https://try.ocamlpro.com/#code/open'Format!!exception'Exit'of'int!!type'info'='FI'of'string'*'int'*'int'$5'UNKNOWN!type'$,a'withinfo'='$4i:'info;'v:'$,a$6!!let'dummyinfo'='UNKNOWN!let'createInfo'f'l'c'='FI(f,'l,'c)!!let'errf'f'=!print_flush();!open_vbox'0;!open_hvbox'0;'f();'print_cut();'close_box();'print_newline();!raise'(Exit'1)!!let'printInfo'=!''(*'In'the'text'of'the'book,'file'positions'in'error'messages'are'replaced!with'the'string'$(Error:$('*)!function!FI(f,l,c)'-$.!print_string'f;!print_string'$(:$(;!print_int'l;'print_string'$(.$(;!print_int'c;'print_string'$(:$(!$5'UNKNOWN'-$.!print_string'$($-Unknown'file'and'line$.:'$(!!let'errfAt'fi'f'='errf(fun()-$.'printInfo'fi;'print_space();'f())!!let'err's'='errf'(fun()-$.'print_string'$(Error:'$(;'print_string's;'print_newline())!!let'error'fi's'='errfAt'fi'(fun()-$.'print_string's;'print_newline())!!let'warning's'=!print_string'$(Warning:'$(;'print_string's;!print_newline()!!let'warningAt'fi's'=!printInfo'fi;'print_string'$('Warning:'$(;!print_string's;'

jimwhite / fib.roc

Created July 2, 2024 22:54

Fibonacci in Roc by ChatGPT

	module [Fibonacci]

	## Returns the Fibonacci sequence up to the nth term.
	fibonacci : U32 -> List U32
	fibonacci = \n ->
	if n == 0 then
	[]
	else if n == 1 then
	[0]
	else

jimwhite / math_notation_2020.html

Created May 17, 2024 05:51

Notation List for Cambridge International Mathematics Qualifications (For use from 2020) converted by GPT-4o to HTML and MathJax

	<!DOCTYPE html>
	<html lang="en">
	<head>
	<meta charset="UTF-8">
	<meta name="viewport" content="width=device-width, initial-scale=1.0">
	<title>Mathematical Notation</title>
	<script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
	<script id="MathJax-script" async src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
	</head>
	<body>

jimwhite / requirements.txt

Created April 19, 2024 21:53

Python 3.11 `pip install lumibot` (3.3.7) then `pip freeze` results

	aiodns==3.2.0
	aiohttp==3.9.5
	aiosignal==1.3.1
	alpaca-py==0.20.3
	alpha-vantage==2.3.1
	annotated-types==0.6.0
	appdirs==1.4.4
	APScheduler==3.10.4
	asttokens==2.4.1
	attrs==23.2.0

jimwhite / requirements.txt

Created April 19, 2024 21:48

Python 3.11 `pip freeze` for https://github.com/Lumiwealth/lumibot at fce4b08

	aiodns==3.2.0
	aiohttp==3.9.5
	aiosignal==1.3.1
	alpaca-py==0.20.3
	alpha-vantage==2.3.1
	annotated-types==0.6.0
	appdirs==1.4.4
	APScheduler==3.10.4
	asttokens==2.4.1
	attrs==23.2.0

Jim White jimwhite