View coq-platform.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
kartik@Kira platform-2021.09.0 % ./coq_platform_make.sh | |
====================== JUST COQ OR COMPLETE PLATFORM ? ======================= | |
This script installs the Coq Platform version 2021.09.0, that is: | |
- the Coq compiler and Coq's standard library | |
- optionally CoqIDE, a GTK3 based graphical user interface | |
- optionally various widely used libraries and plugins | |
- optionally an extended set of libraries and plugins | |
The script uses opam, the OCaml package manager, to do all the work. |
View install-smlnj.sh
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/bin/sh | |
VERSION=${1:-110.97} | |
cd /tmp | |
mkdir -p smlnj && cd smlnj | |
wget http://smlnj.cs.uchicago.edu/dist/working/$VERSION/config.tgz | |
tar -xzf config.tgz | |
mkdir -p ~/.local | |
env INSTALLDIR=~/.local config/install.sh -default 64 |
View snapcraft.yaml
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
name: smlnj | |
title: Standard ML of New Jersey | |
version: "110.97" | |
summary: The Standard ML of New Jersey system | |
description: | | |
Standard ML of New Jersey (abbreviated SML/NJ) is a | |
compiler for the Standard ML '97 programming language | |
with associated libraries, tools, and documentation. | |
https://smlnj.org |
View coqtop killed
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
[52791.541304] coqtop invoked oom-killer: gfp_mask=0x100dca(GFP_HIGHUSER_MOVABLE|__GFP_ZERO), order=0, oom_score_adj=0 | |
[52791.541307] CPU: 6 PID: 17667 Comm: coqtop Tainted: G U 5.2.8-arch1-1-ARCH #1 | |
[52791.541308] Hardware name: Dell Inc. XPS 13 9370/0F6P3V, BIOS 1.11.1 07/11/2019 | |
[52791.541308] Call Trace: | |
[52791.541315] dump_stack+0x5c/0x80 | |
[52791.541318] dump_header+0x51/0x32d | |
[52791.541320] ? preempt_count_add+0x79/0xb0 | |
[52791.541322] ? _raw_spin_lock+0x13/0x30 | |
[52791.541323] ? preempt_count_add+0x79/0xb0 | |
[52791.541324] ? _raw_spin_trylock+0x13/0x50 |
View quipper.sh
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
rm -rf ~/.cabal ~/.stack ~/.ghc ~/.ghcup | |
curl -sSL https://get.haskellstack.org/ | sh | |
stack --resolver lts-7.24 setup | |
stack install cabal-install | |
export PATH=~/.stack/programs/x86_64-linux/ghc-tinfo6-8.0.1/bin:$PATH | |
cabal update | |
cabal install superdoc-0.1.2.3 random-1.1 mtl-2.2.1 primes-0.2.1.0 zlib-0.6.1.2 easyrender-0.1.1.3 Lattices fixedprec newsynth containers set-monad-0.2.0.0 QuickCheck | |
make -j8 | |
quipper/scripts/quipper |
View protoquipper.sh
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
docker build -t="dockerfile/ubuntu" github.com/dockerfile/ubuntu | |
docker run -it dockerfile/ubuntu | |
## Inside the container | |
apt update | |
apt install -y libgmp3-dev freeglut3-dev zlib1g-dev libreadline-dev llvm-3.4 clang | |
wget -c https://downloads.haskell.org/~ghc/7.4.2/ghc-7.4.2-x86_64-unknown-linux.tar.bz2 | |
tar xf ghc-7.4.2-x86_64-unknown-linux.tar.bz2 | |
cd ghc-7.4.2 | |
ln -s /usr/lib/x86_64-linux-gnu/libgmp.so.10 /usr/lib/libgmp.so.3 |
View datalink.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
use pnet::packet::Packet; | |
use pnet::packet::ipv4::{MutableIpv4Packet, Ipv4Packet}; | |
use std::net::{Ipv4Addr, UdpSocket}; | |
use std::sync::mpsc::{self, Sender, Receiver}; | |
use std::thread; | |
// TODO choose a better name for this struct | |
pub struct RouteInfo { | |
// std::net::UdpSocket accepts string in host:port format |
View parallel-cleanup-format
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/usr/bin/env bash | |
# note: clang-tidy only accepts one file at a time, but we can run it | |
# parallel against disjoint collections at once. | |
find . \( -name \*.c -or -name \*.cpp -or -name \*.cc -or -name \*.h \) | xargs -n1 -P4 cleanup-tidy | |
# clang-format accepts multiple files during one run, but let's limit it to 12 | |
# here so we (hopefully) avoid excessive memory usage. | |
find . \( -name \*.c -or -name \*.cpp -or -name \*.cc -or -name \*.h \) | xargs -n12 -P4 cleanup-format -i |
View cleanup-format
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/usr/bin/env bash | |
clang-format -style="{BasedOnStyle: llvm, IndentWidth: 4, AllowShortFunctionsOnASingleLine: None, KeepEmptyLinesAtTheStartOfBlocks: false}" "$@" |
NewerOlder