Slavomir Kaslev skaslev

Effective Modern CMake

Getting Started

For a brief user-level introduction to CMake, watch C++ Weekly, Episode 78, Intro to CMake by Jason Turner. LLVM’s CMake Primer provides a good high-level introduction to the CMake syntax. Go read it now.

After that, watch Mathieu Ropert’s CppCon 2017 talk Using Modern CMake Patterns to Enforce a Good Modular Design (slides). It provides a thorough explanation of what modern CMake is and why it is so much better than “old school” CMake. The modular design ideas in this talk are based on the book [Large-Scale C++ Software Design](https://www.amazon.de/Large-Scale-Soft

Use cases

Textures/Matrices for direct use

Moments In Graphics (void-and-cluster)
2D
3D and 4D
Bart Wronski Implementation of Solid Angle
Forced Random Dithering matrices

This gist shows how formal conditions of Solidity smart contracts can be automatically verified even in the presence of potential re-entrant calls from other contracts.

Solidity already supports formal verification of some contracts that do not make calls to other contracts. This of course excludes any contract that transfers Ether or tokens.

The Solidity contract below models a crude crowdfunding contract that can hold Ether and some person can withdraw Ether according to their shares. It is missing the actual access control, but the point that wants to be made

	open eq

	inductive I (F : Type₁ → Prop) : Type₁ :=
	mk : I F

	axiom InjI : ∀ {x y}, I x = I y → x = y

	definition P (x : Type₁) : Prop := ∃ a, I a = x ∧ (a x → false).

	definition p := I P

	/**
	* Sobol Noise Generation
	* GNU LGPL license
	* By Dr. John Burkardt (Virginia Tech)
	* https://gist.github.com/alaingalvan/af92ddbaf3bb01f5ef29bc431bd37891
	*/

	//returns the position of the high 1 bit base 2 in an integer n
	int getHighBit1(int n)
	{

	// Ray Tracing Gems Chapter 25
	// Code provided by Electronic Arts
	// Colin Barré-Brisebois, Henrik Halén, Graham Wihlidal, Andrew Lauritzen,
	// Jasper Bekkers, Tomasz Stachowiak, and Johan Andersson
	// Errata corrected by Alain Galvan

	struct HaltonState
	{
	unsigned dimension;
	unsigned sequenceIndex;

	namespace cat
	universes u v

	@[class] structure category :=
	(obj : Type u)
	(hom : obj → obj → Type v)
	(cid : ∀ {x : obj}, hom x x)
	(comp : ∀ {x y z : obj}, hom y z → hom x y → hom x z)
	(assoc : ∀ {x y z w} {f : hom x y} {g : hom y z} {h : hom z w},
	comp h (comp g f) = comp (comp h g) f)

	universe variables u v u1 u2 v1 v2

	set_option pp.universes true

	open smt_tactic
	meta def blast : tactic unit := using_smt $ intros >> add_lemmas_from_facts >> repeat_at_most 3 ematch
	notation `♮` := by blast

	structure semigroup_morphism { α β : Type u } ( s : semigroup α ) ( t: semigroup β ) :=
	(map: α → β)

	meta def blast : tactic unit := using_smt $ return ()

	structure Category :=
	(Obj : Type)
	(Hom : Obj → Obj → Type)

	structure Functor (C : Category) (D : Category) :=
	(onObjects : C^.Obj → D^.Obj)
	(onMorphisms : Π { X Y : C^.Obj },
	C^.Hom X Y → D^.Hom (onObjects X) (onObjects Y))

	-- Return the maximum unsigned number of a given width.
	def max_unsigned : ℕ → ℕ
	\| 0 := 0
	\| (nat.succ x) := 2 * max_unsigned x + 1

	open tactic nat

	/- Function for convertiong a nat into a Lean expression using nat.zero and nat.succ.
	Remark: the standard library already contains a tactic for converting nat into a binary encoding. -/
	meta def nat.to_unary_expr : nat → tactic expr