Coq で小数演算

Coq で小数を含む演算を行う。

次のような小数点を含む数値はエラーが出て使えなかった。

Compute 3.3.


そこで、Coq の標準ライブラリ Float で 浮動小数点 の規格 IEEE754 をサポートしている.

IEEE 754 は符号s（0または1）、仮数 c、指数 q の3つの整数で表現し、(−1)^s × c × b^q　
で表される。
Float を使い  c q を設定し、 FtoR 関数を用いて b を決め実数型 R へ変換する.

Require Import Float.Float.
Variable c q b:Z.
Compute (Float c q).
Compute (FtoR b (Float c q).

参考
Mare Daumas, Laurence Rideau, Laurent Thery:A Generic Library of Floating-Point Numbers and its Application to Exact Computing

ftp://ftp-sop.inria.fr/marelle/Laurent.Thery/float.ppt

Manajro Linux で TeamViewer が動かなかった

AUR からTeamViewer を入れてコンソールから TeamViewer を起動させたが起動に失敗した。

理由は Systemd のServiceを起動してないためだった。

そのため、次のようにServiceを起動させることによりTeamViewerが使えるようになった。

$sudo systemctl start teamviewd

ChromeOS に fedora 25 をインストール

ChromeOS で Linux 系 OS を使うにはCroutonで Debian, Ubuntu がよく使われる。
しかし、Debian Ubuntu は入るソフトが古く新しいソフトウェアが使えない、そこで、新しいパッケージを使える Fedora 25　を入れ VNC を使い GUI を実現した。


Fedora インストール方法は下のサイトを参考にした。
https://github.com/nmilosev/crouton-fedora

まず次のコマンドを実行する
$cd ~/Downloads
$wget https://github.com/nmilosev/crouton-fedora/archive/master.tar.gz -O crouton-fedora.tar.gz
$tar xvf crouton-fedora.tar.gz
$sudo sh ./crouton-fedora-master/installer/main.sh -r fedora -t fedora


このとき インストールした Fedore のユーザー名とパスワードはともにfedora になっている。
次にGUI の設定のスクリプトを実行するとハングアップしてしまった
$sudo sh /home/fedora/Downloads/crouton-fedora-master/freon-x/install.sh

そこで、
https://nmilosev.svbtle.com/crouton-with-fedora-chroot-chromebook
を参考にして VNC を使う。

次にwindow Manager を入れるがその前にFedora のパッケージを更新する。この作業を忘れるとパッケージの追加更新の際にエラーがたくさん出るようになった。
$sudo dnf upgrade

今回は Window manager に LXDE を使う
$sudo dnf install @lxde

次にVNC Sever を入れVNCのパスワードを設定する。
$sudo dnf install tigervnc-server
$vncpasswd

次に LXDE を起動する設定をする。
$echo '/usr/bin/startlxde' > ~/.vnc/xstartup && chmod +x ~/.vnc/xstartup

次に、VNCサーバーの起動は
$vncserver :1 -geometry 1360x768 -depth 24

VNC クライアントから
localhost :5901
で起動できる。

opam パッケージのマルチコアビルド

マルチコアでビルドする場合はjobsを使う
opam install --jobs n パッケージ名

--jobs を打ちたくなければ ~/.opam/config の jobs の値を変更する

https://opam.ocaml.org/doc/FAQ.html

crouton で X がエラーが起きて起動できない

Crouton を使った際に X がエラーを起こし起動しなかったの時のメモ

Crouton で Linux を入れた際 startlxde (入れた Window maneger によって違う) を実行しても X が起動しない
enter-chroot をすると Debian/Ubuntu などにログインができる

この場合,クローム拡張を入れていない可能性があるので
https://chrome.google.com/webstore/detail/crouton-integration/gcpneefbbnfalgjniomfjknbcgkbijom
から入れる

私はクローム拡張をいれて Debian 新たに入れたので
X が起動しない状態から拡張を入れ起動するかはわかりません

Common Lisp でGnuplot

数値計算を行った際にグラフの描画が必要になる.
そこで見つけたライブラリの vgplot を紹介する

vgplot は 関数を見る限り 2D グラフの描画しかサポートしていないが簡単に描画することができる.
また,関数名は PLOT, SUBPLOT, TITLE,　XLABEL, AXIS のように Octarve や Matlab ライクな関数名になっている.

https://github.com/volkers/vgplot

ただし,OS X で gnuplot を使う際は  AquaTerm か XQuartz が必要になる

Common Lisp の数値計算ライブラリ2

前回 MatLisp を紹介したが今回も数値計算のライブラリを紹介する

https://github.com/ghollisjr/cl-ana

でこのライブラリは Gnuplot GSL HDL5など科学技術計算に必要なラッパーライブラリを寄せ集めたものであり、
現在も頻繁に保守されているため手軽に使える数値計算ライブラリであることは変わらない