Skip to content

Instantly share code, notes, and snippets.

Paolo G. Giarrusso Blaisorblade

View GitHub Profile
@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.
@Blaisorblade
Blaisorblade / rewrite_iris_funext.v
Created Apr 22, 2020
Rewriting into function applications
View rewrite_iris_funext.v
From iris.algebra Require Import ofe.
Instance equiv_ext_discrete_fun {A B} :
subrelation (≡@{A -d> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance dist_ext_discrete_fun {A B n} :
subrelation (dist n (A := A -d> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
@Blaisorblade
Blaisorblade / NatSem.agda
Last active Apr 21, 2020
Making NatSem compositional and denotational!
View NatSem.agda
module Semwap.NatSem where
open import Prelude hiding (force)
open import Prelude.Extras.Eq
open import Prelude.Extras.Delay
import Level
open import Semwap.Expr
You can’t perform that action at this time.