天泣記

2019-11-29 (Fri)

#1 tig issue

GitHub jonas/tig/issues/973: The line position after 'Move to parent' in tig blame.

2019-11-12 (Tue)

#1 Ruby issue

Ruby Feature #16345: Don't emit deprecation warnings by default.

2019-11-02 (Sat)

#1 Coq issue

Anomaly File 'pretyping/cases.ml', line 2027, characters 2-8: Assertion failed.' with let-in in arity of inductive type #11030

2019-10-29 (Tue)

#1 Coq issue

CArray.fold_right_map scans from left #10987

2019-09-11 (Wed)

#1 TypingFlags に挑戦

TypingFlags をちょっと試してみたが、termination check できない再帰関数の定義はとくに問題なく可能。 でも、そういう関数についてなにか証明するのは(手元の Coq 8.9.1 で試した限りでは)難しい感じ。 証明中に tactic が止まらなくなってしまうことがあって、回避できない。

なんとなく、すべての tactic が確実に止まるようにするのは難しいのだと思うけれど、 証明を作れる程度に改善するのはなんとかなるのではないかという気がする。 Coq 本体に入るとすれば、そのような改善が行われることは期待できる、と思いたい。

2019-09-08 (Sun)

#2 TypingFlags

Coq 開発者との議論のセッションで、今後の Coq 8.10, 8.11 に入る予定の機能が リストアップされていた。

この中で、Coq 8.11 に入る機能に termination check を disable できるようになる、 という話があった。

探してみると、おそらく、TypingFlags のことだと思われる。

#1 Coq Workshop 2019

Coq Workshop 2019 で、 A Gallina Subset for C Extraction of Non-structural Recursion という発表をした。

2019-08-26 (Mon)

#1 pdftimestamp

PDF にドキュメントタイムスタンプ署名をつけるツールを作ってみた。

<URL:https://github.com/akr/pdftimestamp>

まぁ、作った、というよりは PDFBox の example を組み合わせたという感じで、 自分で書いたコードはかなり少ない。

なお、ドキュメントタイムスタンプ署名というのは、Adobe Acrobat だとタイムスタンプという機能に相当し、 手元のドキュメントを TSA(Time Stamping Authority)に署名してもらうというもの。たぶん。



田中哲