kim-em

import Std

/-!
# If normalization

Rustan Leino, Stephan Merz, and Natarajan Shankar have recently been discussing challenge problems
to compare proof assistants.
(See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Rustan's.20challenge)

Their first suggestion was "if-normalization".

kim-em

#!/usr/bin/env python3

import subprocess
import json
import argparse
from collections import defaultdict
from datetime import datetime, timedelta
import re

def run_gh_command(command):

kim-em

% sudo lake env lldb lean Mathlib/SetTheory/Ordinal/Basic.lean
Password:
(lldb) target create "lean"
Current executable set to '/Users/kim/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/lean' (arm64).
(lldb) settings set -- target.run-args  "Mathlib/SetTheory/Ordinal/Basic.lean"
(lldb) run
Process 62488 launched: '/Users/kim/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/lean' (arm64)
Process 62488 stopped
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x42f0010100000000)
    frame #0: 0x0000000107ecf914 libleanshared.dylib`lean_dec_ref_cold + 936

kim-em

#!/usr/bin/env python3

# https://chat.openai.com/share/ee41e766-e16f-4ddc-9ffd-1e984cfc61f5
# https://chatgpt.com/share/4a3157ae-2977-4a2a-93af-93d6396f6f58
import subprocess
import re
import os

opened_files = set()

kim-em

#!/bin/bash

# Initialize counters
warning_count=0
check_count=0
cross_count=0

# Read input, pass it to stdout, and count lines starting with specific characters
while IFS= read -r line; do
    echo "$line"

kim-em

#!/usr/bin/env bash

# Fetch GitHub token using `gh`
GITHUB_TOKEN=$(gh auth token)

REPO_OWNER="leanprover-community"
REPO_NAME="mathlib4"
LABEL="awaiting-review"
PER_PAGE=100
PAGE=1

kim-em

10002
10102
10152
10154
10258
10264
1032
10329
10389
10452

kim-em

10024
10075
10126
10142
10186
10349
10350
10541
10560
10562

kim-em

import Mathlib

/-- Call `sage` -/
def sageOutput (args : Array String) : IO String := do
  IO.Process.run { cmd := "sage", args := args }

/-- Parse a string containing a list of integers. Should be a proper parser! -/
def String.parseNatList (l : String) : List ℕ :=
  (((l.drop 1).dropRight 2).split (. = ' ')).map
    (fun s => s.stripSuffix ",") |> .map String.toNat!

kim-em

import Mathlib

/-- Call `sage` -/
def sageOutput (args : Array String) : IO String := do
  IO.Process.run { cmd := "sage", args := args }

/-- Parse a string containing a list of integers. Should be a proper parser! -/
def String.parseNatList (l : String) : List ℕ :=
  (((l.drop 1).dropRight 2).split (. = ' ')).map
    (fun s => s.stripSuffix ",") |> .map String.toNat!