桜技録

🐈🐈🐈🐈🐘

bash-completionの補完定義はどこに置く?

bash-completion に補完定義を追加するとき、スクリプトファイルはどこにおくべきか。

自ユーザにのみ適用する場合

選択肢①: $XDG_DATA_HOME/bash-completion/completions/*

ディレクト$XDG_DATA_HOME/bash-completion/completions (デフォルトは ~/.local/share/bash-completion/completions )配下に補完したいコマンドと同じ名前のファイルを置いておけば勝手に読み込んでくれる。

なお completions の親ディレクトリは環境変数 BASH_COMPLETION_USER_DIR でカスタマイズ可能。

例) npm コマンドで補完が効くようにする

npm completion >$XDG_DATA_HOME/bash-completion/completions/npm

まずはコレを使うことを考える。

選択肢②: ~/.bash_completions

選択肢①が遅延ロードされるのに対して、こちらはbash-completionの読み込み時に一緒に読み込まれる。

ファイル名は環境変数 BASH_COMPLETION_USER_FILE でカスタマイズ可能。

システム全体に適用する場合

選択肢③: /usr/share/bash-completion/completions/*

ディレクト/usr/share/bash-completion/completions 配下に補完したいコマンドと同じ名前のファイルを置いておけば勝手に読み込んでくれる。

ディストリビューションによってディレクトリは異なる。

選択肢④: /etc/bash_completion.d/*

選択肢③が遅延ロードされるのに対して、こちらはbash-completionの読み込み時に一緒に読み込まれる。

ディストリビューションによってディレクトリは異なる。

ディレクトリは環境変数 $BASH_COMPLETION_COMPAT_DIR でカスタマイズ可能。

SpotBugsでGeneratedアノテーションがついたクラスやメソッドを除外できるようになる

アノテーション・プロセッサ等のツールで自動生成したコードは静的コード解析の対象から外したいもの。

従来SpotBugsの利用者はパッケージやクラスに関する 除外フィルタ の機能を使ってこれに対応してきた。

<!-- これまでの手法 -->
<FindBugsFilter>
  <Match>
    <Package name="com.example.hoge.gen"/>
  </Match>
  <Match>
    <Class name="~.*Entity"/>
  </Match>
</FindBugsFilter>

しかしこの手法では自動生成する成果物のパッケージやクラス名に一定の制約が生じてしまうのは避けられず、またプロジェクトごとに異なる成果物の名前に応じてフィルタを調整しなくてはいけなかった。

その状況が次のSpotBugs 4.8.0(仮)のリリースで変わる。

github.com

新しく AnnotationMatcher なるものを追加するPRがマージされており、「特定のパターンのアノテーションが付いたクラス、メソッド、フィールドを解析対象外にする」といったルールが設定できるようになった。

具体的にはこんな感じ。

<!-- これからの手法 -->
<FindBugsFilter>
  <Match>
    <Annotation name="~.*\.Generated"/>
  </Match>
</FindBugsFilter>

イマドキのコード生成ツールはFQCNはさまざまであるがなにかしらの Generated アノテーションを付けてコード出力するのが常識だと言っていい。

上記のフィルタならばそれら Generated アノテーション付きのコードを解析対象から除外しつつ前述の問題点はすべて解消できる。

新規プロジェクト用のテンプレートに是非反映させたくなるフィルタではないだろうか。

なお次回リリースについてはこちらで議論されている。特定の日付は出てないけれどリリース手順の確認などがなされておりリリースは近い予感。

github.com

配列ではなくオブジェクトからjq select

{
  "045eb00f-e662-4c06-b1ea-052eeefe6307": {
    "name": "hoge",
    "score": 1078
  },
  "85ee1327-aee9-4645-bf01-e035ddfe7ee6": {
    "name": "fuga",
    "score": 961
  },
  "727c03fa-08d2-4fa3-9143-c64f5fc3d404": {
    "name": "piyo",
    "score": 1609
  }
}

エントリのコレクションを配列ではなく上のようにIDをキーとしたオブジェクトで表現したJSONがある。

ここからある条件に合致したエントリ(オブジェクトのメンバ)をjqで抽出するにはどうするか?

to_entries

to_entries を使うとオブジェクトを配列に変換することができる。

jq to_entries
[
  {
    "key": "045eb00f-e662-4c06-b1ea-052eeefe6307",
    "value": {
      "name": "hoge",
      "score": 1078
    }
  },
  {
    "key": "85ee1327-aee9-4645-bf01-e035ddfe7ee6",
    "value": {
      "name": "fuga",
      "score": 961
    }
  },
  {
    "key": "727c03fa-08d2-4fa3-9143-c64f5fc3d404",
    "value": {
      "name": "piyo",
      "score": 1609
    }
  }
]

オブジェクトのメンバを表すオブジェクト {"key": "キー", "value": "値"} を要素とする配列が手に入る。

配列になってしまえば後は select 関数が使える。

# scoreが1000以上のエントリのみ抽出
jq 'to_entries | map(select(1000 <= .value.score))'
[
  {
    "key": "045eb00f-e662-4c06-b1ea-052eeefe6307",
    "value": {
      "name": "hoge",
      "score": 1078
    }
  },
  {
    "key": "727c03fa-08d2-4fa3-9143-c64f5fc3d404",
    "value": {
      "name": "piyo",
      "score": 1609
    }
  }
]

from_entries

from_entries で逆方向の変換もできる。

# scoreが1000以上のエントリのみ抽出
jq 'to_entries | map(select(1000 <= .value.score)) | from_entries'
{
  "045eb00f-e662-4c06-b1ea-052eeefe6307": {
    "name": "hoge",
    "score": 1078
  },
  "727c03fa-08d2-4fa3-9143-c64f5fc3d404": {
    "name": "piyo",
    "score": 1609
  }
}

macOSでCHMファイルを閲覧する

Windowsでのヘルプでお馴染みCHMMicrosoft Compiled HTML Help)をMacで読みたくなった。

以前は ichm なるツールがあったようだが、公式サイトのドメインが売りに出されており信頼できるバイナリの入手元が不明で、また自前でビルドしようにも手が掛かりそう(リポジトリにはXcode用のプロジェクト・フォルダが転がってるだけ)だったので他を探した。

github.com

こちらを導入してみる。

READMEにある通りSourceForgeにある同名プロジェクトは誰かが勝手に作ったものだそうなのでそちらからバイナリを落としたりしないこと(怖っ)。

Mac用のバイナリは提供されないので自前ビルドする。

必要なもの

ライブラリ

いずれもHomebrewで導入可。

brew install chmlib wxwidgets

今回は最新版であるCHMLIB 0.40とwxWidgets 3.1.5を利用した。

ツール

  • autoconf
  • automake

こちらもHomebrewで導入可。

brew install autoconf automake

ビルド

リポジトリをcloneしたディレクトリ直下で下記を行う。

  1. ./bootstrap を実行
  2. ./configure && make を実行

生成された実行可能ファイル src/xchmmac/Info.plistmac/xCHM.icns を次のように配置するとLaunchpadにxCHMが表示される。

/Application/xCHM.app/Contents
├── Info.plist
├── MacOS
│   └── xchm
└── Resources
    └── xCHM.icns

利用

起動するとウィンドウが立ち上がるのであとはメニュー等を見て操作する。

手元で試した限りではコンテンツが日本語のCHMはもちろん、ファイル名が日本語であっても問題なく閲覧できた。

ノート: 情報科学における論理④

小野寛晰『情報科学における論理』の読書ノート。なるべく練習問題も解いてく。(→前回)

第2章 述語論理(承前)

古典述語論理の形式体系LK

推論規則

古典命題論理での推論規則に加えて次の推論規則を持つ。なお  A は論理式、  \Gamma , \Delta は論理式の列、  t は任意の項、  z は対象変数を表す。

∀ Left (∀L)
 \cfrac { A [ t / x ] , \Gamma \vdash \Delta } { \forall x A , \Gamma \vdash \Delta }
∀ Right (∀R)
 \cfrac { \Gamma \vdash \Delta , A [ z / x ] } { \Gamma \vdash \Delta , \forall x A }
∃ Left (∃L)
 \cfrac { A [ z / x ] , \Gamma \vdash \Delta } { \exists x A , \Gamma \vdash \Delta }
∃ Right (∃R)
 \cfrac { \Gamma \vdash \Delta , A [ t / x ] } { \Gamma \vdash \Delta , \exists x A }

∀Rと∃Lを適用するには、  z が下式で自由な出現を持ってはならない。この条件を変数条件(eigenvariable condition)と呼び、また  z 固有変数(eigenvariable)と呼ぶ。

Cut除去定理

命題論理と同様、述語論理のLKに於いてもcut除去定理が成り立つ。

決定不能

命題論理と異なり、与えられた式が述語論理のLKで証明可能かどうかは決定不能

完全性定理

完全性と健全性

命題論理と同様、述語論理のLKも健全かつ完全。

形式理論

閉じた論理式の集合を形式理論(formal theory)または理論と呼ぶ。

理論  T に含まれる論理式からなる有限列  \Sigma を適当に選んで、式  \Sigma , \Gamma \vdash \Delta がLKで証明可能になるとき、  \Gamma \vdash \Delta  T で証明可能といい、  T \vdash ( \Gamma \vdash \Delta ) で表す。(この本が式の導出記号を  \vdash でなく  \rightarrow で記述しているのはこういうことかー。式を構成する記号か、公理から式を導出可能なこと表す記号か紛らわしいね)

 T \vdash ( \vdash ) のとき、つまり式  \Sigma \vdash が証明可能なとき  T 矛盾する(inconsistent)という。

モデル

言語  \mathscr{ L } 上の理論  T  \mathscr{ L } に対する構造  \mathfrak{ A } について、任意の  P \in T  \mathfrak{ A } \models P であるとき、  \mathfrak{ A }  T のモデルと呼ぶ。

二変数述語記号として  = が与えられているとき、次の論理式の集合を等号の公理と呼ぶ。以降同記号を含む言語上の理論には等号の公理が含まれるものとする。

  •  \forall x ( x = x )
  •  \forall x \forall y ( x = y \rightarrow y = x )
  •  \forall x \forall y \forall z ( ( x = y \land y = z ) \rightarrow x = z )
  •  \forall x_1 \cdots \forall x_m \forall y_1 \cdots \forall y_m ( ( x_1 = y_1 \land \cdots \land x_m = y_m ) \rightarrow f ( x_1 , \cdots , x_m ) = f ( y_1 , \cdots , y_m ) )  (  f  m 変数関数記号)
  •  \forall x_1 \cdots \forall x_m \forall y_1 \cdots \forall y_m ( ( x_1 = y_1 \land \cdots \land x_m = y_m ) \rightarrow ( P ( x_1 , \cdots , x_m ) \rightarrow P ( y_1 , \cdots , y_m ) ) )  (  P  m 変数熟語記号)

例として次の記号からなる言語  \mathscr{ L }_1 を考える。

  • 対象定数:  e
  • 一変数関数記号:  ^{-1}
  • 二変数関数記号:  \cdot
  • 二変数述語記号:  =

等号の公理に加えて次の論理式からなる  \mathscr{ L }_1 上の理論  T_1 があるとする。

  •  \forall x \forall y \forall z ( ( x \cdot y ) \cdot z = x \cdot ( y \cdot z ) )
  •  \forall x ( e \cdot x = x \land x \cdot e = x )
  •  \forall x ( x \cdot x^{ -1 } = e \land x^{ -1 } \cdot x = e )

これは明らかに群の定義である。ある群  G があり、その単位元や演算を  \mathscr{ L }_1 の各記号に対応させる写像  I を取れば、構造  ( G , I )  T_1 のモデルになる。また  T_1 のモデルはひとつの群を自然に定める。従ってしばしば群  G と構造  ( G , I ) を同一視する。

強い形の完全性
  1. 任意の理論  T がモデルを持つならば、  T は無矛盾である。
  2. 任意の理論  T が無矛盾ならば、  T はモデルを持つ。

2番を強い形の完全性定理という。

練習問題

問2.13

f:id:sciencesakura:20211204181436p:plain

問2.14

f:id:sciencesakura:20211204182302p:plain

問2.15

2-a)  \forall x B \equiv \forall y ( B [ y / x ] )

f:id:sciencesakura:20211204182642p:plain  f:id:sciencesakura:20211204182657p:plain

2-b)  \exists x B \equiv \exists y ( B [ y / x ] )

f:id:sciencesakura:20211204183439p:plain  f:id:sciencesakura:20211204183500p:plain

3-a)  A \land \forall x B \equiv \forall ( A \land B )

f:id:sciencesakura:20211204183939p:plain  f:id:sciencesakura:20211204183959p:plain

3-b)  A \lor \exists x B \equiv \exists x ( A \lor B )

f:id:sciencesakura:20211204184238p:plain  f:id:sciencesakura:20211204184255p:plain

4-a)  A \lor \forall x B \equiv \forall x ( A \lor B )

f:id:sciencesakura:20211204184710p:plain  f:id:sciencesakura:20211205031724p:plain

4-b)  A \land \exists x B \equiv \exists x ( A \land B )

f:id:sciencesakura:20211205031816p:plain  f:id:sciencesakura:20211205031846p:plain

5-a)  \forall x B \land \forall x C \equiv \forall x ( B \land C )

f:id:sciencesakura:20211205031951p:plain  f:id:sciencesakura:20211205032022p:plain

5-b)  \exists x B \lor \exists x C \equiv \exists x ( B \lor C )

f:id:sciencesakura:20211205032116p:plain  f:id:sciencesakura:20211205032149p:plain

6-a)  ( \forall x B \lor \forall x C ) \rightarrow \forall x ( B \lor C )

f:id:sciencesakura:20211205032257p:plain

6-b)  \exists x ( B \land C ) \rightarrow ( \exists x B \land \exists x C )

f:id:sciencesakura:20211205032329p:plain

10-a)  \lnot \forall x B \equiv \exists x \lnot B

f:id:sciencesakura:20211205032655p:plain  f:id:sciencesakura:20211205032740p:plain

10-b)  \lnot \exists x B \equiv \forall x \lnot B

f:id:sciencesakura:20211205032832p:plain  f:id:sciencesakura:20211205032858p:plain

11-a)  A \rightarrow \forall x B \equiv \forall x ( A \rightarrow B )

f:id:sciencesakura:20211205034117p:plain  f:id:sciencesakura:20211205034130p:plain

11-b)  A \rightarrow \exists x B \equiv \exists x ( A \rightarrow B )

f:id:sciencesakura:20211205035656p:plain  f:id:sciencesakura:20211205035732p:plain

12-a)  \forall x B \rightarrow A \equiv \exists x ( B \rightarrow A )

f:id:sciencesakura:20211205040801p:plain  f:id:sciencesakura:20211205041237p:plain

12-b)  \exists x B \rightarrow A \equiv \forall x ( B \rightarrow A )

f:id:sciencesakura:20211205042811p:plain  f:id:sciencesakura:20211205043425p:plain

13)  \exists x ( B \rightarrow C ) \equiv \forall x B \rightarrow \exists x C

f:id:sciencesakura:20211205044708p:plain  f:id:sciencesakura:20211205045725p:plain

14)  \forall x ( B \rightarrow C ) \rightarrow ( \forall x B \rightarrow \forall x C )

f:id:sciencesakura:20211205050415p:plain

15)  \forall x ( B \rightarrow C ) \rightarrow ( \exists x B \rightarrow \exists x C )

f:id:sciencesakura:20211205050857p:plain

Oracle 18c XE on CentOS 7.9 on VirtualBoxセットアップ

自分用の作業記録。

  • CentOS 7.9 (2009)
  • Oracle Database Express Edition Release 18.4.0.0.0

仮想マシン構成

  • メモリ: 4096 MB
  • ストレージ: 16 GB VDI (Dynamically allocated)
  • ネットワーク1: NAT
  • ネットワーク2: Host-only Adapter (DHCP disabled)

Oracle XEのインストールに際してインターネットからの依存パッケージのDLが発生する為NATでインターネット・アクセスを可能にする。

ホストマシンからDBへ接続が行えるようHost-only Adapterを追加している。なおホストマシンからは固定IPでアクセスしたいのでDHCPは使わない。

ゲストOSインストール

https://www.centos.org/centos-linux/ からDLしたインストール・メディア(DVDタイプ)をIDEバイスに追加して仮想マシンを起動。GUIインストーラが立ち上がる。

[INSTALLATION SOURCE] 、 [INSTALLATION DESTINATION] はデフォルトのまま。 [SOFTWARE SELECTION] には Minimal Install を指定した。

[NETWORK & HOSTNAME] を開いてアダプタが2つ認識されていることを確認。 enp0s3enp0s8 という名前が付いていた。

enp0s3の接続をONにするとHost-only Adapterのネットワーク・アドレスには乗らないIPアドレスが振られていたのでNATの方のアダプタだと判明。

もう一方のenp0s8は接続がONにできない。 [IPv4 Settings] を開き、 [Method] に Manual を指定、 [Additional static addresses] にHost-only Adapterに適合するゲートウェイサブネットマスクIPアドレスを追加する。これで接続をONにできる。

あとは流れに沿ってインストールを進める。

ホストマシンからの接続確認

インストール後の再起動が済んだらホストマシンからsshでリモート・ログインを試みる。インストーラでネットワーク設定を終わらせておいたので繋がると思ったが失敗。

VirtualBoxのウィンドウからログイン、 ip addr してみる。

1: lo: <LOOPBACK,UP,LOWER_UP> mtu 65536 qdisc noqueue state UNKNOWN group default qlen 1000
    link/loopback 00:00:00:00:00:00 brd 00:00:00:00:00:00
    inet 127.0.0.1/8 scope host lo
       valid_lft forever preferred_lft forever
    inet6 ::1/128 scope host
       valid_lft forever preferred_lft forever
2: enp0s3: <BROADCAST,MULTICAST,UP,LOWER_UP> mtu 1500 qdisc pfifo_fast state UP group default qlen 1000
    link/ether 08:00:27:4e:db:2d brd ff:ff:ff:ff:ff:ff
    inet 10.0.2.15/24 brd 10.0.2.255 scope global noprefixroute dynamic enp0s3
       valid_lft 86388sec preferred_lft 86388sec
    inet6 fe80::a00:27ff:fe4e:db2d/64 scope link
       valid_lft forever preferred_lft forever
3: enp0s8: <BROADCAST,MULTICAST,UP,LOWER_UP> mtu 1500 qdisc pfifo_fast state UP group default qlen 1000
    link/ether 08:00:27:11:f1:63 brd ff:ff:ff:ff:ff:ff

enp0s8にIPアドレスが振られていない。 nmtui でenp0s8の設定を確認すると何故か [Automatically connect] にチェックが付いていなかった。チェックを付けて systemctl restart NetworkManager する。

ip addr でenp0s8に固定IPが表示されること、ホストマシンからssh接続できることを確認する。

Oracle XEインストール

マニュアルに従って実施。

https://docs.oracle.com/en/database/oracle/oracle-database/18/xeinl/procedure-installing-oracle-database-xe.html

https://docs.oracle.com/en/database/oracle/oracle-database/18/xeinl/setting-oracle-database-xe-environment-variables.html

自動起動の設定

OSが立ち上がったらOracle XEも起動するようにする。

chkconfig --add oracle-xe-18c

ファイアウォールの設定

デフォルトでOracleのリスナが使う1521番ポートへ外部(ホストマシン)から接続ができるようにする。

firewall-cmd --permanent --add-port=1521/tcp
firewall-cmd --reload

Raspberry Pi 4Bの有線+固定IP+headlessセットアップ

キーボード/ディスプレイなしでラズパイをセットアップした作業記録。作業PCはmacOS

PC上での作業には💻、リモート接続したラズパイ上での作業には🥧を以下見出しに付ける。

💻 OSインストール

導入するのはGUIレスで軽量なRaspberry Pi OS Lite。

公式のDLページからOSイメージのzipを入手、解凍する。

PCにSDカードを挿す前と後で diskutil list でディスク一覧を表示、使用するSDカードのデバイス・ファイル名を確認する。

dd コマンドでOSイメージをSDカードに焼く。書き込み先には上で確認したデバイス・ファイルを指定すること。

# SDカードをアンマウント
diskutil unmountDisk /dev/disk2

# イメージをコピー
sudo dd bs=1M if=2020-08-20-raspios-buster-armhf-lite.img of=/dev/rdisk2; sync

コピーが終わると /Volumes/boot が見えるようになる。

[参考] https://www.raspberrypi.org/documentation/installation/installing-images/mac.md

💻 SSHを有効化

touch /Volumes/boot/ssh で空ファイルを作る。起動時に /boot/ssh というファイルがあればSSHサービスが有効になる仕組み。

[参考] https://www.raspberrypi.org/documentation/remote-access/ssh/README.md

💻 Bluetooth / Wi-Fiを無効化

無線を使うつもりがないので切った。/boot/config.txt に下を設定する。

# Bluetoothを無効
dtoverlay=disable-bt

# Wi-Fiを無効
dtoverlay=disable-wifi

パラメータの詳細や他に設定可能なパラメータ等は /boot/overlays/README に記載アリ。

💻 起動+SSH接続

SDカードをラズパイに挿し、LANケーブルに繋いで電源を投入する。

緑色LEDの点滅が落ち着き起動し終えたと思われるタイミングでPCからSSH接続する。初期パスワードは raspberry

ssh pi@raspberrypi.local

🥧 aptアップグレード

近場のサイト(ここではJAIST)をミラーサイト一覧から探して /etc/apt/sources.list のURLを置き換える。

すべてのパッケージを最新化する。

sudo apt-get update \
  && sudo apt-get -y upgrade \
  && sudo apt-get -y dist-upgrade \
  && sudo apt-get -y autoremove \
  && sudo apt-get autoclean

🥧 rasp-configアップグレード

Raspberry Pi OSの設定ツールrasp-configを最新化。sudo rasp-config で起動するとメニューが立ち上がるので [Update] を選択する。

🥧 ロケールを設定

rasp-configで設定。[Localisation Options] > [Change Locale] で言語に en_US.UTF-8 を、[Localisation Options] > [Change Time Zone] でタイムゾーンAsia/Tokyo を設定する。

※再起動するまで反映されない。

🥧 ホスト名を変更

rasp-configで設定。[Network Options] > [Hostname] でホスト名を変更する。

※再起動するまで反映されない。

🥧 IPアドレスを固定

/etc/dhcpcd.conf に下を設定する。

interface eth0
static ip_address=192.168.11.2/24        # IPアドレス/サブネットマスク
static routers=192.168.11.1              # デフォルト・ゲートウェイ
static domain_name_servers=192.168.11.1  # DNSサーバ

※再起動するまで反映されない。

LAN内でDHCPを運用している場合はIPアドレスが衝突しないようDHCPの付番範囲外のアドレスを使うこと。

[参考] https://www.raspberrypi.org/documentation/configuration/tcpip/README.md

🥧 再起動+設定確認

sudo reboot でOSを再起動する。

新しいIPアドレスSSH接続出来ることを確認する。

新しいホスト名がプロンプトに表示されていることを確認する。

指定したロケールlocale コマンドで表示されることを確認する。

無線LANインタフェース wlan0ip link コマンドで表示されないことを確認する。

適当なデバイスでそれらしいBluetoothが飛んでいないことを確認する。

💻 known_hostsのゴミを掃除

IP変える前に接続した時のゴミが ~/.ssh/known_hosts に残るので消しておく。

ssh-keygen -R raspberrypi.local