Proof-Generalを用いたCoqの環境構築

はじめに 久々に Coq で遊びたくなったので、M1 Mac にインストールしてみた。 最近の Coq は VSCode で書くのが主流?らしいが、今回は Emacs + Proof-General で環境構築を行う。 環境構築の方法 基本的にbrewやmelpaなどの package 管理システムになるべく依存した形で環境構築を行う。 はじめに、Coqのインストール(–build-from-source をつけないとcoqtop実行時にエラーが出た。) brew install coq --build-from-source GUI 版 Emacs のインストール brew install emacs --cask Emacs の設定 次は Emacs の設定を行う。 Emacs の設定ファイルは~/.emacs.d/init.elに記載する。 まずはmelpa(Emacs のプラグインのパッケージマネージャー)のセットアップを行う。 ~/.emacs.d/init.elに以下を記載し、 (require 'package) (let* ((no-ssl (and (memq system-type '(windows-nt ms-dos)) (not (gnutls-available-p)))) (proto (if no-ssl "http" "https"))) (add-to-list 'package-archives (cons "melpa" (concat proto "://melpa.org/packages/")) t)) (package-initialize) emacs を起動して...

October 23, 2022 · 1 min · 200 words · derbuihan

i7 870にTensorflowの環境構築方法

はじめに 落ちてた i7 870 のパソコンにグラボを 2 枚刺して、機械学習専用サーバーを作りました。 このとき、最新の Tensorflow をインストールしても使えないので苦労しました。 これは i7 870 は Sandy Bridge 以前の CPU なので AVX 命令がないのが原因です。 この記事では i7 870 でも機械学習が出来るように、少し古めの Tensorflow の環境を構築する方法を解説します。 この情報は 2020 年 12 月に出来た方法です。 前提 CUDA 10.2 Nvidia Driver Version: 440.100 Anaconda をインストール tensorflow v1.5.0 のインストール方法 はじめに、仮想環境の作成 $ conda create -n tf1 python==3.7 anaconda $ conda activate tf1 tensorflow-gpu v1.15.0 を指定してインストール $ conda install -c anaconda tensorflow-gpu==1.15.0 $ conda install -c anaconda keras ついでに、tensorflow-datasets をインストール(conda で入るのはバージョンが古いので pip でインストール)...

December 18, 2020 · 1 min · 174 words · derbuihan

MacでCoqのバージョンを指定してインストール

いつものように $ brew update && brew upgrade してたら coq の version が 8.9.0 になってしまい、今まで書いていたコードが動かなくなったので、coq の version を 8.8.2 にします。 ほとんど ↓ の記事を見ながらやりました。 参考: Homebrew で旧バージョンのパッケージをインストールしたい brew でバージョン指定してインストールする方法 ローカルに Coq がある場合 $ brew info coq を実行して version 8.8.2 がローカルに残っているなと思ったら $ brew switch coq 8.8.2 で coq の version を変えれるらしいです。 ローカルに Coq がない場合 まず、 $ cd /usr/local/Homebrew/Library/Taps/homebrew/homebrew-core/Formula $ git log coq.rb で適当に指定の version を見つける。 commit ef92c34e061cb99920f7ae05d3ba205fccc5f1b8 Author: BrewTestBot <homebrew-test-bot@lists.sfconservancy.org> Date: Wed Oct 31 17:08:20 2018 +0000 coq: update 8....

February 14, 2019 · 1 min · 131 words · derbuihan

Root権限がない環境で色々インストールする。

Root なしで人権を得る方法です。 Tmux をビルドする。 こんな素晴らしい記事がある。 これをコピペして実行。 linuxbrewを用いる。 以下を~/.bashrcに追加して再度ログイン。 if [ ! -r ~/.linuxbrew ]; then git clone https://github.com/Linuxbrew/brew.git ~/.linuxbrew fi if [ -r ~/.linuxbrew ]; then export PATH="$HOME/.linuxbrew/bin:$HOME/.linuxbrew/sbin:$PATH" export MANPATH="$MANPATH:$HOME/.linuxbrew/share/man" export INFOPATH="$INFOPATH:$HOME/.linuxbrew/share/info" #export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:$HOME/.linuxbrew/lib" fi

January 12, 2019 · 1 min · 35 words · derbuihan

Atomで入れるプラグイン一覧

随時更新していきます。 通常編 とりあえず Atom をインストールしたら入れるプラグイン atomic-emacs Atom で Emacs のキーバインドを使う。 japanese-menu 設定を日本語化 platformio-ide-terminal Ctrl-`で下からターミナルが出てくるようになる。 project-manager project を管理できるようになる。 LaTex 環境編 tex を Atom で書くときのプラグイン一覧。 language-latex シンタックスハイライト latex tex のコンパイル latexer 補完 pdf-view pdf を見れるようになる。 感想 Atom で Coq やりたい。 Atom では Vim より Emacs のが使いやすい。

December 29, 2018 · 1 min · 44 words · derbuihan