Xiaohu Zhu tigerneil

I am no longer abe to monitor this post , I have decided to move everything to my personal blog for better monitoring.

Please click here to access the full post

Ubuntu 22.04 for Deep Learning

In the name of God

This gist contains steps to setup Ubuntu 22.04 for deep learning.

Install Ubuntu 22.04

How to deal with quotients or setoids?

Lean

Lean extends the Calculus of Inductive Constructions with quotient types, as discussed by Carneiro (2019, Sec 2.7.1). However, that and other choices break some metatheoretic properties of CIC (Carneiro, 2019, Sec. 3.1), properties that Coq developers care about; consistency is nevertheless preserved.

Coq

Coq does not add support for quotients; one must instead use setoids explicitly. By looking at Carneiro (2019), we can see the difference: unlike quotient A/R, a setoid (A, R) is not a standard type, and we must explicitly remember to use R instead of standard equality wherever needed. Both with setoids and quotients, we must ensure that functions respect the equivalence on their domain. However, when using quotients A/R, that must only be checked for functions that use A/R's eliminator, while with setoids we need more work. For example, take a function f : A/R -> B, and g : B -> C: we can

Setting up a MSI laptop with GPU (gtx1060)

Installing Ubuntu 18.04, CUDA, CDNN, Pytorch and TensorFlow

Installing Ubuntu 18.04

Get Image

https://tutorials.ubuntu.com/tutorial/tutorial-create-a-usb-stick-on-ubuntu#0

Install (solving issues)

Reset mysql root password in Mac OS:

First Stop MySQL:

Go to: 'System Preferences' >> 'MySQL' and stop MySQL

OR,

sudo /usr/local/mysql/support-files/mysql.server start
sudo /usr/local/mysql/support-files/mysql.server stop

	// An example of using the PyTorch C++ API to implement a custom forward and backward function

	#include <iostream>
	#include <vector>

	#include <torch/torch.h>
	#include <torch/csrc/autograd/variable.h>
	#include <torch/csrc/autograd/function.h>
	#include <torch/csrc/autograd/VariableTypeUtils.h>
	#include <torch/csrc/autograd/functions/utils.h>

	from selenium import webdriver
	from selenium.webdriver.support.ui import WebDriverWait
	from selenium.webdriver.common.by import By
	from selenium.webdriver.support import expected_conditions as EC
	import requests
	import os


	def download_all_papers(base_url, save_dir, driver_path):
	driver = webdriver.Chrome(driver_path)

	import keras
	import numpy as np

	timesteps = 60
	input_dim = 64
	samples = 10000
	batch_size = 128
	output_dim = 64

	# Test data.

	{-# LANGUAGE GADTs #-}
	{-
	The following code is based on experimental code by Aslan Askerov
	based on Ramsey and Pfeffers "Stochastic Lambda Calculus and Monads of
	Probability Distributions". Implementation of random n is from
	Audebaud and Paulin-Mohring paper, so is the random walk example.

	This gist is used here http://madsbuch.com/the-probability-monad/

	The class hierarchy is as follows: