lean_new

#!/bin/sh
#
# shellcheck disable=SC2086 # deliberate splitting
# shellcheck disable=SC2059 # deliberate format variable
# shellcheck disable=SC2142 # deliberate function in alias
# shellcheck disable=SC2317 # code is reachable; shellcheck is wrong
# 
# Usage: lean_new PROJECT
#   Creates new Lean 4 project named PROJECT in current directory
#   with mathlib dependency and an executable default target.
#
#   It tries to ensure that lake and elan have the expected behavior
#   in order for the project to build and informs the user of any known
#   pitfalls.

## Preliminaries
set -u

unset -v raw_chars pascal upper

r='\033[31m' #red
b='\033[34m' #blue
g='\033[32m' #green
d='\033[1m'  #bold
s='\033[0m'  #reset

out() { printf '%s\n' "$@"; }

__errex() {
	fatal_string="${d}Fatal error [$r%s$s$d] on line $g%s$s$d in '$b%s$s$d':$s %s\n"
	printf "${fatal_string}"               \
		"${1:-"?"}"                        \
		"${2:-"?"}"                        \
		"${3:-"undetermined script"}"      \
		"${4:-"undetermined error"}" >&2   ;
	exit "${1:-1}"
}
alias die='__errex "$?" "${LINENO}" "$0"'

__outex() {
	abandon_string="${d}Abandoning script '$b%s$s$d' at line $g%s$s$d with code [$r%s$s$d]:$s %s\n"
	printf "${abandon_string}"             \
		"${1:-"undetermined script"}"      \
		"${2:-"?"}"                        \
		"${3:-"?"}"                        \
		"${4:-"undetermined reason"}" >&2  ;
	exit "${3:-1}"
}
alias bye='__outex "$0" "${LINENO}" "$?"'

set_raw_chars() {
	smash="$*"
	raw_chars=
	while [ -n "${smash}" ]; do
		remains="${smash#?}"
		raw_chars="${raw_chars}${smash%%"${remains}"} "
		smash="${remains}"
	done
}

set_pascal() {
	set_upper() {
		case "$*" in
			a) upper="A" ;; b) upper="B" ;; c) upper="C"  ;;
			d) upper="D" ;; e) upper="E" ;; f) upper="F"  ;;
			g) upper="G" ;; h) upper="H" ;; i) upper="I"  ;;
			j) upper="J" ;; k) upper="K" ;; l) upper="L"  ;;
			m) upper="M" ;; n) upper="N" ;; o) upper="O"  ;;
			p) upper="P" ;; q) upper="Q" ;; r) upper="R"  ;;
			s) upper="S" ;; t) upper="T" ;; u) upper="U"  ;;
			v) upper="V" ;; w) upper="W" ;; x) upper="X"  ;;
			y) upper="Y" ;; z) upper="Z" ;; *) upper="$*" ;;
		esac
	}
	set_upper "$1"
	pascal="${upper}"
	shift
	while [ "$#" -gt 0 ]; do
		if [ "$1" = "_" ]; then
			shift
			set_upper "$1"
			pascal="${pascal}${upper}"
		else
			pascal="${pascal}$1"
		fi
		shift
	done
}

## Initial checks

out "-- Checking elan default toolchain..."

elan toolchain list | tee /dev/tty | grep -qFe 'stable (default)' || {
	out "----------------------------------------------" \
		"Warning: default elan toolchain is not stable!" \
		"Always install elan with the stable toolchain." \
		"----------------------------------------------" \
		"Continue anyway? "                              ;

	read -r response || die "Unable to read response."

	case "${response}" in
		y|Y|yes|Yes|YES) :            ;;
	  	*) bye "rejecting toolchain." ;;
	esac
}

grep -qE '^[[:alnum:]_]+$' <<NAME || die "invalid characters in project name."
$*
NAME

set_raw_chars "$*"
set_pascal ${raw_chars}

## Confirm project creation

out "-------------------------" \
    "Current directory: ${PWD}" \
    "Project name : $*"         \
    "Pascal name  : ${pascal}"  \
    "-------------------------" \
    "Is this ok? "              ;

read -r response ||
die "Unable to read response."

case "${response}" in
	y|Y|yes|Yes|YES) :                ;;
	*) bye "rejecting project names." ;;
esac

lake new "$*" math ||
die "command 'lake new' failed."

cd "$*" ||
die "cannot cd to new directory."

mv -f lakefile.lean lakefile.original

cat <<LAKEFILE >| lakefile.lean || die "unable to write new lakefile."
import Lake
open Lake DSL

package «$*» where
  -- Settings applied to both builds and interactive editing
  leanOptions := #[
    ⟨\`pp.unicode.fun, true⟩ -- pretty-prints \`fun a ↦ b\`
  ]
  -- add any additional package configuration options here

lean_lib «${pascal}» where

/-!
  mathlib ensures batteries, Cli, Qq, aesop, proofwidgets and importGraph
-/
require alloy   from git "https://github.com/tydeu/lean4-alloy.git"
require mathlib from git "https://github.com/leanprover-community/mathlib4.git"

@[default_target]
lean_exe $* where
  root := \`Main
LAKEFILE

out "-- Created new lakefile; if the build fails, check syntax compatibility." \
    "-- The original file generated by lake is 'lakefile.original'."           ;

out 'def main : IO Unit :=' '  IO.println "Clean main!"' >| Main.lean ||
die "failed to create Main.lean"

out "-- Directory ready; trying to build..."

## Try build

lake build &&
./.lake/build/bin/$*

exit