Skip to content

Instantly share code, notes, and snippets.

John Bender johnbender

View GitHub Profile
@johnbender
johnbender / LibTactics.v
Last active Jan 10, 2017
Coq 8.6 and Software Foundations Fix
View LibTactics.v
(*
The error while running `make` is:
File "./LibTactics.v", line 3238, characters 17-18:
Syntax error: ')' expected after [constr:lconstr] (in [tactic:tactic_arg]).
The fix to line 3238 is below.
*)
Ltac branch_tactic K N := (* Line 3237 *)
View keybase.md

Keybase proof

I hereby claim:

  • I am johnbender on github.
  • I am johnbender (https://keybase.io/johnbender) on keybase.
  • I have a public key whose fingerprint is 61FA 972A F856 C432 2573 D4AD C9B0 1EF5 DE6A 1098

To claim this, I am signing this object:

View gist:f49457abfa0a21feff06
Sorry, doesn't handle recursion (function c::tmalloc_releaseAllReverse; .cpp) identifier not found
Sorry, doesn't handle recursion (.h)
View gist:def97c0a69d39de08658
vagrant@vagrant-ubuntu-trusty-64:/vagrant/scratch/rstm$ ../goto-cc -o run.gb run.cpp -Iinclude
file /usr/include/c++/4.8/cstdlib line 178: parse error before `__int128 abs ( __int128'
file /usr/include/c++/4.8/cstdlib line 183: parse error before `} namespace __gnu_cxx {'
file /usr/include/c++/4.8/cstdlib line 236: parse error before `} namespace std {'
file /usr/include/c++/4.8/cstdlib line 254: parse error before `} typedef unsigned char'
file include/common/locks.hpp line 77: parse error before `: "memory" ) ;'
file /usr/lib/gcc/x86_64-linux-gnu/4.8/include/xmmintrin.h line 91: parse error before `0.0f , 0.0f ,'
file /usr/lib/gcc/x86_64-linux-gnu/4.8/include/xmmintrin.h line 92: parse error before `} extern __inline __m128'
file /usr/lib/gcc/x86_64-linux-gnu/4.8/include/xmmintrin.h line 102: parse error before `} extern __inline __m128'
file /usr/lib/gcc/x86_64-linux-gnu/4.8/include/xmmintrin.h line 108: parse error before `} extern __inline __m128'
View review.md
View keybase.md

Keybase proof

I hereby claim:

  • I am johnbender on github.
  • I am johnbender (https://keybase.io/johnbender) on keybase.
  • I have a public key whose fingerprint is 56AD FEE0 8B4D F194 1E76 DF77 5BFB 243D 5898 7620

To claim this, I am signing this object:

@johnbender
johnbender / Vagrantfile.rb
Last active Dec 22, 2015
If you'd rather not install Node.
View Vagrantfile.rb
# -*- mode: ruby -*-
# vi: set ft=ruby :
# Vagrantfile API/syntax version. Don't touch unless you know what you're doing!
VAGRANTFILE_API_VERSION = "2"
Vagrant.configure(VAGRANTFILE_API_VERSION) do |config|
config.vm.box = "precise64"
config.vm.provision(:shell, :inline => <<-CMD)
@johnbender
johnbender / prefs.js
Created Feb 23, 2013
Set up Chrome Secure Shell to handle solarized terminal colors
View prefs.js
// Disable bold.
term_.prefs_.set('enable-bold', false)
// Use this for Solarized Dark
term_.prefs_.set('background-color', "#002b36");
term_.prefs_.set('foreground-color', "#839496");
term_.prefs_.set('color-palette-overrides', [
'#073642',
'#dc322f',
@johnbender
johnbender / foo.sh
Last active Dec 13, 2015
Replace a sed match with file contents.
View foo.sh
replace=foo
replace_with=bar.txt
replace_in=baz.txt
sed -i.bkp "/$replace/{
s/$replace//g
r $replace_with
}" $replace_in
You can’t perform that action at this time.