Arnaud Spiwack aspiwack

Replace Pulseaudio

Ubuntu 21.04 comes with Pipewire pre-installed. A pipewire service is running, but it’s doesn’t handle audio by default. For this you need to install a pipewire-pulse service. The (preinstalled) pipewire package provides such a service as documentation. First let’s copy it in Systemd’s space.

$ cp /usr/share/doc/pipewire/examples/systemd/user/pipewire-pulse.* /usr/lib/systemd/user/

Keybase proof

I hereby claim:

I am aspiwack on github.
I am aspiwack (https://keybase.io/aspiwack) on keybase.
I have a public key ASAdUTbPKE_sXn1PUR6IItRsYY6oaQki2LSvqSdZsCkntgo

To claim this, I am signing this object:

	MAIN_END_PAGE = 25

	%-submission.pdf: %.pdf
	pdftk $< cat 1-$(MAIN_END_PAGE) output temp.pdf
	pdftk $< dump_data_utf8 \| pdftk temp.pdf update_info_utf8 - output $@
	rm -f temp.pdf

	{-# LANGUAGE DerivingVia #-}
	{-# LANGUAGE LinearTypes #-}
	{-# LANGUAGE NoImplicitPrelude #-}

	-- \| This module turns every monoid into a (linear) comonoid.
	--
	-- It generalises the Writer monad, since `tell` is `consume . spend`.
	--
	-- It looks a lot like the following twisted (applicativg) functor (see also
	-- https://dl.acm.org/doi/abs/10.1145/2976002.2976004 /

	module Cdcl where

	import Data.Foldable
	import Data.Maybe
	import Data.Monoid

	type Atom = Int

	type Literal = (Bool, Atom)

	module CatList : sig

	(** “Lazy” lists with O(1) concatenation. *)
	type +'a t

	type (+'a, +'l) view =
	\| Nil
	\| Cons of 'a * 'l

	val view : 'a t -> ('a, 'a t) view

	;; I wrote a bit of Emacs configuration (which can be added to your
	;; init.el) so that an lhs2tex file can be syntax-highlighted as a
	;; Latex file but the Haskell code is highlighted as Haskell code. In
	;; fact it's a little more than this, as the code blocks are
	;; interpreted with the haskell-mode, so you can use your haskell
	;; commands there.
	;;
	;; I don't recommend opening all `.lhs' file in this mode, as they
	;; don't need to be Latex files. Literate Haskell is really agnostic
	;; about its surrounding language.

	(** A small STG-like lazy abstract machine. What I take from the STG
	is that constructors are responsible for choosing a branch in a
	pattern-matching (the T in STG) and for updating themselves (by
	pushing an update frame). Apart from that it's not very different
	from a simple KAM. Note that the current implementation in GHC is
	not actually tagless anymore, as it proved to be slower than a
	tagged mechanism. But since it's a simpler design, (and the
	difference doesn't matter much unless actual machine code is
	emitted).

	(** To give a direct proof of the constructive result that [forall
	A:Prop, ~~(A\/~A)], it is useful to see [~A] as meaning a
	"continuation of [A]". That is, [~A] is a computation that takes an
	[A] and "returns".*)

	(** Here is a first proof by forward chaining. *)
	Lemma Proof₁ : forall A:Prop, ~~(A\/~A).
	Proof.
	intros A k₀.
	(** We have [k₀:~(A\/~A)]. That is [k₀] is a continuation of either

	PKG core_bench
	PKG qcheck
	B _build