Skip to content

Instantly share code, notes, and snippets.

Avatar

Paolo G. Giarrusso Blaisorblade

View GitHub Profile
@Blaisorblade
Blaisorblade / oddity.txt
Created Aug 27, 2020 — forked from paulp/oddity.txt
Whitespace Oddity
View oddity.txt
WHITESPACE ODDITY
by Paul Phillips, in eternal admiration of David Bowie, RIP
Bound Ctrl to Major mode
Bound Ctrl to Major mode
Read inputrc and set extdebug on
Bound Ctrl to Major mode (Ten, Nine, Eight, Seven, Six)
Connecting readline, options on (Five, Four, Three)
Check the syntax, may terminfo be with you (Two, One, Exec)
View The Signs of Soundness
Hello scala, my old friend
I've come to take you home again
Because a feature slowly creeping
left me plagued with doubts and weeping
and the version that was tagged in the repo
just has to go
it lacks the signs of soundness
On sleepless nights I hacked alone
applying ant and other tools of stone
@Blaisorblade
Blaisorblade / crouton.init
Last active Jul 17, 2020 — forked from DennisLfromGA/crouton.init
An external control file for adjusting four parameters in 'crouton.conf' to invoke a crouton chroot.
View crouton.init
##########################################################################
##* crouton.conf defaults are: ##
# DELAY=10 # delay desired number of seconds before starting ##
# CHROOT=xenial # enter desired chroot to start ##
# START_DE=startxfce4 # enter desired Desktop Envirnoment to use ##
# CHROOT_APP=none # enter desired chroot application to run ##
# XMETHOD=default # enter the desired XMETHOD (xorg,xephyr,xiwi) ##
# RUN_STATE=y # change to 'n' to disable running $CHROOT ##
##########################################################################
@Blaisorblade
Blaisorblade / crouton.conf
Last active Jul 17, 2020 — forked from DennisLfromGA/crouton.conf
A ChromeOS upstart script to kick-off a crouton chroot desktop environment.
View crouton.conf
# Copyright (c) 2016 The crouton Authors. All rights reserved.
# Use of this source code is governed by a BSD-style license that can be
# found in the LICENSE file.
## Filename: /etc/init/crouton.conf
## NOTE: 'rootfs' verification needs to be removed.
## crouton chroot - Start session
##
## This will start a (crouton) chroot Desktop Environment session
@Blaisorblade
Blaisorblade / rw-rootfs
Last active Jul 17, 2020 — forked from DennisLfromGA/rw-rootfs
A script that asks to make the root filesystem read-writable for subsequent changes and additions by the user.
View rw-rootfs
#!/bin/sh -e
##!! PLEASE USE THIS SCRIPT WITH CAUTION - AND AT YOUR OWN RISK !!##
##!! IT HAS BEEN KNOWN TO CAUSE RESETS AND WIPE DATA ON SOME CHROMEBOXES !!##
APPLICATION="${0##*/}"
ANSWER=''
SUDO=''
USAGE="
$APPLICATION [no options]
@Blaisorblade
Blaisorblade / tweakbusproofs.sty
Created Jul 11, 2020
Tune output from busproofs to be closer to mathpartir
View tweakbusproofs.sty
% Ensure that bussproofs and mathpartir rules have the same thickness.
%
% bussproofs uses hrule, defaulting to 0.4pt. Instead, testing and docs show
% that mathpartir uses \over, both by default and here.
% Horizontal rule thickness for \over depends on font parameters.
%%
% Read the thickness of fraction rule.
%%
% 1. We use https://tex.stackexchange.com/a/96063/1340 to read font parameters.
% 2. The parameter in question is \fontdimen8\textfont3,
View gist:541416169b97729e60bb80fb0f259b7d
1: looking for (Equiv (hoD Σ n)) without backtracking
1.1: (*external*) (eapply (ofe_equiv _)) on (Equiv (hoD Σ n)), 0 subgoal(s)
1: looking for (Equiv (hoLtyO Σ n)) without backtracking
1.1: (*external*) (eapply (ofe_equiv _)) on
(Equiv (hoLtyO Σ n)), 0 subgoal(s)
1: looking for (Proper (equiv ==> equiv) packHoLtyO) without backtracking
1: looking for (Params (@packHoLtyO) ?H0) with backtracking
1.1: exact Params_instance_1 on (Params (@packHoLtyO) ?H0), 0 subgoal(s)
1.1: (*external*) proper_reflexive on
(Proper (equiv ==> equiv) packHoLtyO), 1 subgoal(s)
@Blaisorblade
Blaisorblade / not_dne_siprop.v
Created May 14, 2020
Show that with step-indexing, double-negation elimination is false
View not_dne_siprop.v
From iris.si_logic Require Import siprop bi.
(** Taken from [base_logic.bi]. *)
(** New unseal tactic that also unfolds the BI layer.
TODO: Can we get rid of this? *)
Ltac unseal := (* Coq unfold used to circumvent bug #5699 in rewrite /foo *)
unfold bi_emp; simpl; unfold sbi_emp; simpl;
unfold siProp_emp, bupd, bi_bupd_bupd, bi_pure,
bi_and, bi_or, bi_impl, bi_forall, bi_exist,
bi_sep, bi_wand, bi_persistently, sbi_internal_eq, sbi_later; simpl;
@Blaisorblade
Blaisorblade / hints.v
Created May 10, 2020
two identical Coq hints
View hints.v
(*external*) (simple apply @label_pair_iapprox_persistent)(level 1, pattern
@Persistent (uPredI (iResUR ?Σ))
(@iapprox ?Σ ?Hdlang (prod label ?A)
(@label_pair_iapprox ?Σ ?Hdlang ?A ?B)
?x ?y), id 0)
simple apply @label_pair_iapprox_persistent(level 1, pattern
@Persistent (uPredI (iResUR ?META11068))
(@iapprox ?META11068 ?META11069 (prod label ?META11070)
(@label_pair_iapprox ?META11068 ?META11069 ?META11070 ?META11071)
View fractionalR.v
From iris.base_logic Require Import invariants.
(* From iris.bi Require Import ascii. *)
From iris.algebra Require Import ofe cmra frac agree gmap.
Definition fractionalR (o : ofeT) : cmraT := prodR fracR (agreeR (leibnizO o)).
Lemma fractional_op A p q (rv : agreeR (leibnizO A)) :
(p, rv) ⋅ (q, rv) ≡ ((p + q)%Qp, rv).
Proof. by rewrite -pair_op agree_idemp. Qed.
Section sec.
You can’t perform that action at this time.