Enigma Lav lovely-error

AMD

Create this file sudo touch /etc/apt/sources.list.d/rocm.list
put this line in there deb [arch=amd64] https://repo.radeon.com/rocm/apt/3.5.1/ xenial main
sudo apt update
install ocl sudo apt install rocm-opencl3.5.0
this script doesnt write icd path to /etc/OpenCL/vendors/ so that's on us
touch /etc/OpenCL/vendors/amdocl64.icd
echo "/opt/rocm-3.5.1/opencl/lib/libamdocl64.so" > /etc/OpenCL/vendors/amdocl64.icd
done. run clinfo. thing should work at this point

	import Batteries


	def NModB251CC8 := Vector (Fin 251) 4
	def MAX_VAL := (250 * 251^0) + (250 * 251^1) + (250 * (251 ^ 2)) + (250 * (251 ^ 3))
	def NModSC := Fin (MAX_VAL + 1)

	def from_NModB251CC8_to_Nat : NModB251CC8 -> Nat \| i => (i.zipWithIndex.map (fun ⟨ a , i ⟩ => a * ((251:Nat) ^ i))).foldl Nat.add 0

	example : from_NModB251CC8_to_Nat (Vector.mk #[250,250,250,250] (by decide)) < MAX_VAL + 1 := by trivial

	#![feature(ptr_metadata)]
	// use libc; // 0.2.159
	use std::alloc::Layout;
	use std::ptr::copy_nonoverlapping;
	use std::mem::forget;
	use std::ptr::metadata;
	use std::ptr::DynMetadata;

	fn main() {

	def zmod : Nat -> Type \| n => Quot (fun a b => a % n = b % n)

	theorem prop_true_or_false : (p:Prop) -> p = False ∨ p = True := by
	exact fun p => Or.symm (Classical.propComplete p)

	theorem quot_ctor_inj : Quot.mk f a = Quot.mk f b -> a = b := by
	intro k
	-- injection k
	admit

	example {x:Rat} : 3 * x / 0.2 = (2 + 1/2) / (3 + 1/3) -> x = 1/20 := by
	let is1 : (0.2:Rat) = 1/5 := by rfl
	rw [is1]
	let is2 : 3 * x / (1/5) = 3 * x * 5 := by
	simp_all only [one_div, div_inv_eq_mul]
	rw [is2]
	let is3 : 3 * x * 5 = 15 * x := by
	calc
	3 * x * 5 = 3 * 5 * x := mul_right_comm 3 x 5
	3 * 5 * _ = 15 * x := by

	def wmap : Type _ -> Type _ -> Type _ :=
	fun A B => @Subtype (Prod (A -> B) (B -> A)) fun ⟨ f , h ⟩ => ∀ i, h (f i) = i


	def p1 : (w:wmap A B) -> let ⟨ ⟨ _ , h ⟩ , _ ⟩ := w; ∀ a:A , @Subtype B fun b => h b = a := by
	intro w
	let ⟨ ⟨ f , h ⟩ , p ⟩ := w
	simp at p
	simp
	intro a

	{-# OPTIONS --type-in-type #-}

	open import Agda.Builtin.Nat
	open import Agda.Builtin.Bool

	data Prod (L R : Set) : Set where
	pair : L -> R -> Prod L R

	data Unit : Set where
	pt : Unit

	// for given number N, this function finds another number K such that
	// (N * K) mod 2^64 = 1
	fn mult_mod_inv(n: u64) -> u64 {
	assert!(n & 1 == 1, "Doesnt work for even numbers");
	assert!(n != 0, "Equation 0 mod N == 1 does not have a solution");
	let mut k = 1u64;
	let mut i = 1u64;
	for _ in 0 .. 64 {
	i <<= 1;
	let c = k.wrapping_mul(n);