Skip to content

Instantly share code, notes, and snippets.

View zunction's full-sized avatar

Zhangsheng Lai zunction

6 followers · 11 following
View GitHub Profile
@zunction
zunction / 0-4-steps-get-docker-with-gpu-on-ubuntu-2004.md
Created November 22, 2022 07:24 — forked from hideojoho/0-4-steps-get-docker-with-gpu-on-ubuntu-2004.md
4 steps to get a docker running with GPU on Ubuntu 20.04

⚠️ The following instruction is written on 25 Jul 2020 (= old).

4 steps to get a docker running with GPU on Ubuntu 20.04

Environment

  • Ubuntu 20.04
  • CUDA 10.2
  • Docker Latest
@zunction
zunction / csv_list.txt
Last active September 27, 2022 08:58
SP DVPY datasets
http://www.weather.gov.sg/files/dailydata/DAILYDATA_S44_201901.csv
http://www.weather.gov.sg/files/dailydata/DAILYDATA_S44_201902.csv
http://www.weather.gov.sg/files/dailydata/DAILYDATA_S44_201903.csv
http://www.weather.gov.sg/files/dailydata/DAILYDATA_S44_201904.csv
http://www.weather.gov.sg/files/dailydata/DAILYDATA_S44_201905.csv
http://www.weather.gov.sg/files/dailydata/DAILYDATA_S44_201906.csv
http://www.weather.gov.sg/files/dailydata/DAILYDATA_S44_201907.csv
http://www.weather.gov.sg/files/dailydata/DAILYDATA_S44_201908.csv
http://www.weather.gov.sg/files/dailydata/DAILYDATA_S44_201909.csv
http://www.weather.gov.sg/files/dailydata/DAILYDATA_S44_201910.csv
@zunction
zunction / astronauts.sql
Created May 5, 2021 03:49 — forked from pamelafox/astronauts.sql
NASA astronauts, 1959-Present
/* Source:
https://www.kaggle.com/nasa/astronaut-yearbook
*/
CREATE TABLE astronauts(
Name TEXT PRIMARY KEY,
Year INTEGER,
GroupNum INTEGER,
Status TEXT,
Birth_Date TEXT,
Birth_Place TEXT,
@zunction
zunction / pokemon.sql
Created March 11, 2021 06:30 — forked from pamelafox/pokemon.sql
Pokemon statistics
CREATE TABLE pokemon(
Number INTEGER,
Name TEXT PRIMARY KEY,
Type_1 TEXT,
Type_2 TEXT,
Total INTEGER,
HP INTEGER,
Attack INTEGER,
Defense INTEGER,
Sp_Atk INTEGER,
@zunction
zunction / utils.hs
Last active June 8, 2020 16:00
reflkg utils
import System.IO
import Control.Monad
type Node = Prelude.String
-- singleton inductive, whose constructor was Node
node_rect :: (Prelude.String -> a1) -> Node -> a1
node_rect f =
f
@zunction
zunction / reflect_query_type.v
Created April 27, 2020 16:24
From mathcomp Require Import all_ssreflect.
From void Require Import void.
From deriving Require Import deriving.
Require Import Coq.Strings.String.
Open Scope string_scope.
(* Deriving the type structures of string *)
Canonical string_indType := Eval hnf in IndType _ _ [indMixin for string_rect].
@zunction
zunction / new.v
Last active April 24, 2020 08:56
WFH copy paste gist
From mathcomp Require Import all_ssreflect.
From void Require Import void.
From deriving Require Import deriving.
Require Import Coq.Strings.String.
Open Scope string_scope.
(* Deriving the type structures of string *)
Canonical string_indType := Eval hnf in IndType _ _ [indMixin for string_rect].
@zunction
zunction / pred_type.v
Last active April 28, 2020 07:42
Code sharing to SW with reflection proofs
From mathcomp Require Import all_ssreflect.
From void Require Import void.
From deriving Require Import deriving.
Require Import Coq.Strings.String.
Open Scope string_scope.
(* Deriving the type structures of string *)
Canonical string_indType := Eval hnf in IndType _ _ [indMixin for string_rect].
@zunction
zunction / sw_pred.v
Last active April 5, 2020 03:04
Working with preds for KGs
From mathcomp Require Import all_ssreflect.
From void Require Import void.
From deriving Require Import deriving.
Require Import Coq.Strings.String.
Open Scope string_scope.
Section uri.
@zunction
zunction / tings_pred.v
Created March 31, 2020 09:12
From mathcomp Require Import all_ssreflect.
Inductive Ting := a | b | c | d | aa | bb | cc | dd | default.
Scheme Equality for Ting.
Lemma eq_TingP : Equality.axiom Ting_beq.
Proof. by do 2!case; constructor. Qed.
Definition Ting_eqMixin := Equality.Mixin eq_TingP.
Canonical Ting_eqType := Equality.Pack Ting_eqMixin Ting.
Definition query_pred := pred Ting.