MLLex と MLYacc を Poly/ML に移植

SML

移植 MLLex と MLYacc を Poly/ML で使えるように移植しました。 移植と言うよりは使える状態のリポジトリを作って Makefile とか書きましたというだけですが、やはりこの二つは重要なので使える状態で維持したいですね。 移植先のリポジトリは eldesh/mllex…

SML のドキュメント生成ツール SMLDoc をサルベージした

SML

SMLDoc は SML# プロジェクトの一部として開発されていたドキュメント生成ツールです。 SMLコードのコメント中に書いた内容を、そのコメントに対応するエンティティに紐付けて表示するようなHTMLを生成します。昔の SML# には SMLDoc が同梱されていましたが…

SMLUnit のインストールを統一して簡潔にした

SML

SML用のユニットテストライブラリとして SMLUnit というライブラリがあります。 SML# プロジェクトの一部として開発されたようですが、現在は SML# 以外の処理系向けのコードは独立したリポジトリで管理されています。現在対応している処理系は以下の4つです…

SMLでSHA3を実装しました

SML

SHA(3)はNISTが定めたセキュアなハッシュアルゴリズムの標準規格です。 今回SHA2のSML実装に続きSMLでSHA3を実装し、SHA3SMLとして公開しました。現在のところSML/NJ 110.99で動作を確認しています。 実装状況 SHA3SMLは直接FIPS 202を確認して実装しました…

並列ML: MaPLe v0.2 がリリースされていた

POPL 2021 の論文 Provably Space-Efficient Parallel Functional Programming が出たのに合わせて2020年末*1にMaPLe v0.2 がリリースされていました。 前回の POPL の時は aobench を動かす記事 並列ML: MaPLe で AObench を高速化 を書きました。MaPLe(mpl…

MDN の JavaScript building blocks を読み終えた

前回 に引き続き JavaScript の構成要素 を読みました。 if, for, while, イベント, イベントリスナ、イベントハンドラ などが導入されました。 文中の練習問題はテキストエリアに入力されたコード片がインタラクティブにその場に反映されるというものなので…

MDN の JavaScript First Steps を読んだ

JavaScriptを勉強することにしました。 ECMAScriptという名前で呼ばれていない時点で気にくわないものであることは確定なんですが、学ぶのが妥当という判断になってしまいました。まずMDNのJavaScriptの第一歩という教材を一通り読んで課題をやりました。 Ja…

並行システムの検証と実装を読んだ

序 CSP(Communication Sequential Process)というプロセス代数とそれに基づいた形式手法の本を読みました。頑張って読んだので紹介します。 CSPは並行計算をラベル付き遷移システムで表現した上で(これをプロセスという)、どのような遷移がありうるのか、プ…

SML#のDockerイメージが全種揃った

eldesh/smlsharp で公開しているSML#のdockerイメージがあります。 最近必要になって バージョン1 系列(1.0.0, 1.0.1, 1.0.2, 1.0.3, 1.1.0)を追加しました。今月初め頃 0.90 をビルドしてあったため、 これで現時点でのリリースを全種揃えたことになりまし…

SML/NJのdockerイメージをマルチアーキテクチャ対応した

私が個人的に管理しているsml/njのdockerイメージを linux/amd64 と linux/386 のマルチアーキテクチャ対応しました。 以下のページでタグを確認すると、linux/amd64 と linux/386 という種類が表示されると思います。> eldesh/smlnj/tags 使用方法 使用する…

SMLUnitをPoly/MLに対応した

SMLUnitというSML用ユニットテストライブラリをPoly/ML5.8から使えるようにしました。 makeと上手く連携するMakefileが書けたので満足です。 ブランチはここ> https://github.com/eldesh/SMLUnit/tree/support/polyml *1使い方はReadmeに書いたけど、Poly/ML…

SML# 版 AObench をMassiveThreadsで高速化

SML

前回*1はちょっとケチが付いてしまいましたが、今回めげずに AObenchSML の SML# 版に MassiveThreads による並列化版 を追加しました。 シングルスレッド版と並列化版を両方実行します。 並列forを実装して 並列ML: MaPLe で AObench を高速化 で作ったもの…

SML#のプログラムにMassiveThreadsのオプションを付けるとパフォーマンスが低下する

SML

SML# には最初からユーザレベルの細粒度スレッドライブラリ MassiveThreads のラッパーが提供されています。 Myth ストラクチャを使ってプログラムを書き、環境変数 MYTH_NUM_WORKERS で仕様コア数を指定するようです。 > 11.2 MassiveThreadsを用いた細粒度…

並列ML: MaPLe で AObench を高速化

SML

POPL2020 で新しい並列ML(MaPLe)(略称: MPL)の提案がありました。 正確に言うと言語の提案じゃ無くて、「並列プログラムの性質を表す(良い)性質 Disentanglement Property を提案したので、その良さ(= 並列プログラムの実行効率)を示すための処理系を作って…

nfq_bind_pf の使い方

Linux にはネットワークフィルタリング機能と、そのラッパーライブラリである libnetfilter-queue があります。 そのライブラリの提供するAPIである nfq_bind_pf と nfq_unbind_pf は uint16_t pf を要求します。 これに何を渡せばいいのかよく判らなかった…

GitHub Actions で Github Pages を更新する方法

github actions でビルドした内容で github pages で公開しているサイトを更新する方法をメモ。 環境+要件 案1: github-push-action 案2: actions-gh-pages 採用案 環境+要件 github 上のパブリックリポジトリである gh-pages ブランチを github pages とし…

Github Actions を勉強した

今後覚えざるを得なさそうだったのでリポジトリを作ったついでに Github Actions を勉強して使ってみました。 勘や常識(を出来るだけ)無しに公式ドキュメントに書いてある内容のみで理解することを目標にしましたが、ちょっとつらかった。とりあえずビルドは…

coqdocを使った

coqdocを初めて使ってみました。はじめは company-coq のスタイルに合わせて見出しとか書いてましたが、なんとなく気が向いたので公式(documenting-coq-files-with-coqdoc )の方を確認してみたのでした。目的はcoqスクリプトの(主にコメントの)整形スタイル…

静的コード解析の会#9

(会場と日程を変更しました) #静的コード解析の会 第9回 - connpass に行ってきました。今回も何らかの発表は出来ず。 どこかで宣伝したらしく、前回から人数が大幅に増えて14~5人くらいの参加者でした。参加者の傾向としては: なぜかIsabelle使いが多い。 …

RustでマルチスレッドWebサーバを作る例を写経

Final Project: Building a Multithreaded Web Server - The Rust Programming Languageを写経した。 標準ライブラリのみを使って簡単なマルチスレッドWebサーバを書く例。 スレッドプールを作ってacceptするたびに「htmlを応答する関数」をJobとしてチャン…

ブログ引っ越し完了

滑り込みではてなダイアリーから引っ越し完了しました。 移行が簡単に出来るのは素晴らしいですね。デザインはこれから横幅がいっぱいに使えるヤツをゆっくり探します。

歯が痛くて倒れていた

8月中旬頃、突然奥歯(の中の神経)に激痛が起こりました(結局明確な原因は不明)。 2週間くらいしてようやく普通の生活が出来るようになりました。あまりに酷い状態だったので書き留めておきます。 どんな状態だったかというと: 常に痛い。何もして無くても神…

terraformのチュートリアルを読んだ

terraformのチュートリアルを一通り読んで実行した。 チュートリアルを実行するのに必要な知識が全てチュートリアル内にあり、かなり分かりよい ほぼ写経で動く(1度AWSのよく分からないエラーが出たけど) 記述が古い箇所がある(動きはする) その時点でのconf…

静的コード解析の会#6で発表してきた

静的コード解析の会#6でVeriFastによる停止性検査について発表してきました。(資料作って徹夜してしまった…) 前回も同じテーマでしたが私の理解も資料も十分でなかったため(α)としてました。 が、今回の発表では多重集合、整礎関係、実際の処理系で検査でき…

SMLでSHA2アルゴリズムを実装しました

SML

SMLでSHA2(Secure Hash Algorithm)というハッシュアルゴリズムを実装しました。 https://github.com/eldesh/sha2_sml.gitに公開してあります。現在のところSML/NJで動作を確認しています。 #こういう基本的な部品から実装して行くのが重要です。たぶん。 実…

定理証明支援系 matita のdockerイメージを作った

Matitaという定理証明系のdockerイメージを作りました。 MatitaはBologna(ボローニャ)大学で作られた、OCaml(+lablgtk)製の、依存型に基づく定理証明器です。 Leanの論文から参照されていたので知りました。 定理証明器の研究用途に作成されたようなので実用…

SMLUnitのインストールを通してSML/NJ向けのライブラリのインストール方法を解説する

SML/NJにはCM(CompilationManager)というビルドツールが付いてきます。 以前は基本的な使い方を書きました>CompileManager(SML用make)の使い方。今回の記事ではSMLUnitというユニットテストライブラリを例にCMで管理するライブラリのインストール方法を説明…

MLtonのdockerイメージを作りました

SMLの最適化コンパイラであるMLtonのDockerイメージを作りました。MLtonは開発は行われているのですが、長らくリリースが出ていないため使いづらい状態です。あとなぜか私の手元だとビルドに失敗したりします*1。 そこで現状の開発ヘッドをビルドしたイメー…

VeriFastのDockerイメージを作りました

C言語/Java検証器であるVeriFastのDockerイメージを公開しました。 > https://hub.docker.com/r/eldesh/verifast/ 現時点(2017/8/24)での開発ヘッドをビルドしてあります*1。リリース版は公式サイトでバイナリが配布されているのでそちらを使いましょう。こ…

SML#3.3.0のDockerイメージを作った

Dockerの練習として SML#3.3.0 の入ったDockerイメージを作ってみました。> https://hub.docker.com/r/eldesh/smlsharp/ $ docker pull eldesh/smlsharp:3.3.0 とやれば使えるはず。ベースイメージは centos:centos7.3.1611 です。 LLVMのサイズが強敵でした…