AnbLnの日記

AnbLn@ぽりえすてるのブログ

日記0013とバグメモ

8月29日 (水)

継続は力なり。

私は無力なのでブログを続けられない。。。

前回は6月19日なので70日ぶりの更新です


最近はNO MAN'S SKYというPS4のゲームにはまっております。
宇宙の星から星へ宇宙船一つで飛び回る壮大なゲームです。

このゲームのうたい文句が『1,844京の惑星』です。
自分が発見した惑星には自分で名前をつけてアップロードもできるんです。

チュートリアルも丁寧ですし、あとバグも盛り沢山です(笑
宇宙とオープンワールドが好きなら是非遊んでみてください

バグメモ

SKLabelNode表示されない問題

node.color = UIColor.black

としていた箇所は正しくは

node.fontColor = UIColor.black

だった。

Coq-math-ssreflect その1

6月19日 (火)

六月発の更新です、、、、
もっと更新しないと、、、、

Coqの勉強をかねてライブラリの説明を日本語に訳します

これで、しばらく記事の内容を考えなくてすむかな、、



mathcomp.ssreflect.eqtype

このファイルでは二つの基礎的なインターフェースを定義します。

eqType : 決定的な等価性をもつ構造
Equality mixins can be made Canonical to allow generic folding
of equality predicates.

一言:数学のあらゆる対象で等号=は当たり前に定義されている。
あまり難しく考えず=が定義されている対象AをA : eqTypeと宣言するとだけ覚えておくと良い。

subType p : {x : T | p x}に同型な構造。
p: pred T (pred は一項関係)



eqTypeでは次の演算が使えます。
x == y : xとyを比較して一致するならtrueを返す
x == y :> T : xとyをT型として比較して一致するならtrueを返す
x != y : xとyを比較して一致するならfalseを返す
x != y :> T : xとyをT型として比較して一致するならfalseを返す
x =P y :: a proof of reflect (x = y) (x == y); this coerces to x == y -> x = y.

comparable T <-> equality on T is decidable := forall x y : T, decidable (x = y)
comparableClass compT == eqType mixin/class for compT : comparable T.
pred1 a : 一点集合 [pred x | x == a].
pred2, pred3, pred4 : 二、三、四点集合
predC1 a : 一点集合の補集合 [pred x | x != a].
[predU1 a & A] : [pred x | (x == a) || (x \in A) ].
[predD1 A & a] : [pred x | x != a & x \in A].
predU1 a P, predD1 P a == applicative versions of the above.
frel f == f : T -> T に対して、[rel x y | f x == y].
invariant k f == elements of T whose k-class is f-invariant.
:= [pred x | k (f x) == k x] with f : T -> T.

[fun x : T => e0 with a1 |-> e1, .., a_n |-> e_n]
[eta f with a1 |-> e1, .., a_n |-> e_n] ==
the auto-expanding function that maps x = a_i to e_i,
and other values of x to e0 (resp. f x).
In the first form the `: T' is optional and x can occur in a_i or e_i.
おそらく、有限個の元の像を指定する関数.

Equality on an eqType is proof-irrelevant (lemma eq_irrelevance).
The eqType interface is implemented for most standard datatypes: bool,
unit, void, option, prod (denoted A * B), sum (denoted A + B),
sig (denoted {x | P}), sigT (denoted {i : I & T}).
We also define tagged_as u v == v cast as T(tag u) if tag v == tag u, else u.

> We have u == v <=> (tag u == tag v) && (tagged u == tagged_as u v).



subTypeの演算はまた今度


参考: mathcomp.ssreflect.eqtype

日記0011とGoogle Analytics導入

5月25日 (金)

今日は大学に行ってゆるめのゼミをやって、帰ってぼーっとしてました。
最近睡眠不足です。
さっさと寝ます。

Google Analytics導入

以下を参考にGoogleAnalyticsを導入しました。

はてなブログにGoogleアナリティクスを設定する手順【2017最新版】 – メモ×マネタイズ=メモタイズ

ブログ書く習慣もついてきたのでね、、、

そろそろブログのアクセス数を増やす努力をしてみようと思います。


アクセス数を増やす目的はアプリの宣伝のためです。

現在、ぽりえすてるは6個のiOSアプリを配信していますが、自信を持って紹介できるのは一つだけです。

アプリ開発モチベーションのためにもアクセス数を増やしたい!!!

といった感じで週末を締めくくります。

次はGoogleアナリティクスでどういう解析すればいいのか調べたいと思います。

日記0010とTeXインストール

5月24日 (木)

今日は、レポートやってTeXをインストールしたら1日が終わりました。

TeXのインストールは結構めんどくさい


TeXをインストールしよう

TeXとかLaTeXとかよく聞きますけど一体どういったものなのでしょうか。

TeX と LaTeX の違い | ラング・ラグー

上の記事によくまとめられているのですが、TeXは組み版処理系やそこで用いられる記述言語のことをいいます。
文字と文字の間隔(カーニングとか)や文章の配置を記述できます。

僕は数学科なので、数式を書くのにも非常によく使います。



下記のページを参考にインストールを進めました。

MacTeX 2018 のインストール&日本語環境構築法 - TeX Alchemist Online

ところが、最後の実験で、うまくpdfが出力されません。😖

そこで下記のページを次に試しました。

macOS High Sierra + Texlive 2017 + ヒラギノフォント - Qiita

そうしたら、実験はうまく成功しました。😌

なんだかAppleに踊らされた気分です。

日記0009とターミナル環境作成メモ

5月22日 (火)

研究室でパソコンを貸与してもらったので、ターミナルで一から開発環境を作っていたが、エラーが起きた



pointer being freed was not allocated

neovim0.2.2で `pointer being freed was not allocated` - TIL blog
neovim does not work on macOS 10.12 Sierra · Issue #18466 · NixOS/nixpkgs · GitHub

開発環境を入れるのそれなりに慣れてるのですが、エラーが起きました。😦

上記のようなエラーが出て、init.vimのdein関連のコードでエラーが発生していました。😥

暗黒美夢王はdeinじゃなくてneovimのバグじゃない?と言っています。
そこで、neovimのプレリリースをダウンロードして解凍して、binにあるnvimを実行したら、無事init.vimを読み込み、deinが実行されました。😊

ここを見ると、homebrewでインストールしたneovimに問題があるとか?🤔

まあ、一度deinを実行できたら、次から大丈夫なのでこれ以上深入りはしませんが、この記事が参考になれば幸いです。



せんでん😘

日記0008と方針変更

5月20日 (日)

FlowerPuzzleのデザインがどうもダメで少し反省してみる

思い返すと、世の中のパズルゲームは幾何学模様を用いていることが多いので、自分もそうしたい

ここで一回足踏みして、幾何学的デザインの研究をしたい

やばたにえん