GCC拡張の無効化 (と、それにまつわる細かい話)

端的に言えば-pedantic-errorsを使えばよい。(できれば-std=...も併用したほうがいいだろう)

以下解説

GCCのC/C++コンパイラは、独自の拡張機能を導入している。これを無効化するオプションには2種類あり、意味が異なる。

1. C標準と矛盾する拡張機能を無効化する。
2. (C標準と矛盾しないかもしれない)拡張機能を無効化する/または警告を出す。

実は、C言語の規格は、それぞれのコンパイラの拡張機能を全面的に禁止しているわけではない。「正しいプログラム(strictly conforming program)を正しく動かす」ことさえ満たせばいいので、いくつかの拡張機能が有効化されたままでも、標準に準拠していると言える場合があるのだ。

C標準と矛盾する拡張機能を無効化する

C標準と矛盾する拡張機能を無効化するには、 -std オプションでISO C/C++を指定すればいい。 C Dialect Options - Using the GNU Compiler Collection (GCC) このオプションは、「C/C++のバージョン」「ISO準拠またはGNU独自」の2つの内容を指定する。

このオプションのデフォルトは、-std=gnu11や-std=gnu++03のように、gnuが含まれている設定である。これには、C標準と矛盾する拡張機能が含まれている。これを-std=c11や-std=c++14のように、cが含まれている設定に変えれば、C標準に準拠した挙動になる。

C標準と矛盾する拡張機能の例

• 1行コメント : C89と矛盾する。一見矛盾しないように見えるが、1行コメントの有無により挙動が変わるコードが存在する。
• Trigraphの無効化 : "??/"のようなコードの解釈が変わる。
• typeof : C++11以降のdecltypeに相当する機能。このような予約語をC標準の範囲内で追加することはできない(変数名と衝突する可能性があるからである)。同じ機能をもつ__typeof__は問題ない。

多くのGCC拡張機能は、既存のCコードの意味を変えないように配慮されている。したがって、この方法で拡張機能を無効化することによる影響はそれほど大きくはない。

拡張機能を無効化する/または警告を出す

• 拡張機能に警告を出すには、 -Wpedantic オプション*1を使う。 C Dialect Options - Using the GNU Compiler Collection (GCC)
• 拡張機能をエラーにするには、-pedantic-errors オプションを使う。

これは、C/C++コード中で拡張機能が利用されていた時に、警告またはエラーにする機能である。

このオプションの挙動も明快に説明できるわけではなく、色々な注釈が必要である。

• long longなど、「以前のバージョンではGCC拡張であったが、新しいバージョンでは標準」という機能は多数存在する。これらは、-std=c...で指定されたバージョンに応じて判定する。
• -std=gnu...が指定されていた場合は、対応するISO C/C++標準に基づいて判定する。しかし、-pedantic-errorsを指定していても、例えば-std=c90と-std=gnu90では意味が違う。上記の1行コメントの例は、前者ではコンパイルが通るが、後者ではコンパイルエラーになる。
• -Werror=pedanticとすると、-Wpedanticで出る警告すべてをエラーにすることができる。これは-pedantic-errorsとは微妙に意味が異なる。*2
• 明示的に「拡張機能」とされているものを判定することはできるが、これによってプログラムが本当の意味でISO C/C++準拠であるかを確認できるとは限らない。
  • コンパイル時にわかる範囲の例では、int _Foo = 1;のようなコードを規格違反として検出できない。*3
  • 処理系定義・未規定・未定義な挙動により、「たまたま動いているけど動く保証がないコード」が生まれることはよくある。これを全てコンパイル時に検出するのは不可能である。実行時にある程度検出することはできる (デバッグオプションで説明されている-fsanitize=undefinedオプションなど) が、完全ではないし、実行効率が落ちると予想される。

*1:Wがない -pedantic も同じ意味

*2:とドキュメントには書いてあるが、詳細は未調査

*3:その部分が標準ライブラリ由来であるか、ユーザーの提供したプログラム由来であるかを判定するには、コンパイラの構造をそれなりに変えないといけないので、将来のコンパイラでもこれを判定することはないだろう。

64bit windows上でのalloy* (hola)

Alloy (hola) のバックエンドはSATソルバであり、いくつかのバックエンドから選べる。しかし、64bit windows上の64bit JREでは、SAT4J以外は動作しない。

以下の手順で自分でjarを作成すれば、minisat等が動くバイナリが作れる。

kodkodのネイティブライブラリをダウンロードして展開

/some/path$ wget http://alloy.mit.edu/kodkod/release/win_x86_64.zip
/some/path$ unzip win_x86_64.zip

Alloyをダウンロードして展開

/some/path$ wget http://alloy.mit.edu/alloy/hola/downloads/hola-0.2.jar
/some/path$ mkdir hola-0.2
/some/path$ cd hola-0.2
/some/path/hola-0.2$ jar xvf ../hola-0.2.jar

kodkodのネイティブライブラリをコピー

/some/path/hola-0.2$ cp -r ../win_x86_64 amd64-windows

jarを作成

/some/path/hola-0.2$ jar cvfm ../hola-0.2.jar META-INF/MANIFEST.MF .

以上により、64bit windows用のネイティブライブラリが含まれたhola-0.2.jarが作成された。

C++11 random 覚え書き

C++11以降では<random>ヘッダで良質な擬似乱数を得ることができる。

#include <random>

外部からの乱数

外部から乱数を得るにはrandom_deviceを使う。

#include <random>
#include <iostream>

int main() {
  std::random_device rand_dev;
  std::cout << rand_dev() << std::endl;
  std::cout << rand_dev() << std::endl;
  return 0;
}

上のように、外部からの乱数源は関数として呼び出すことで乱数を生成する。

このプログラムは実行するごとに異なる値を出力する。

擬似乱数

擬似乱数は、シード値を放り込むと乱数っぽい数列を吐き出すプログラム。

生成方法が何種類かあるが、mt19937だけ把握していればよい。

#include <random>
#include <iostream>

int main() {
  std::mt19937 rand_src(12345);
  std::cout << rand_src() << std::endl;
  std::cout << rand_src() << std::endl;
  return 0;
}

上のように、擬似乱数生成器は関数として呼び出すことで擬似乱数を生成する。

このプログラムは異なる整数を2つ出力するが、プログラムの実行ごとに同じ整数を出力する。

ソース中の12345がシード値である。この数値を変更すると、異なる整数を出力するようになる。

乱数の加工

上で生成した乱数は32bit一様乱数等なので、必要な分布が出るように加工する。

#include <random>
#include <iostream>

int main() {
  std::mt19937 rand_src(12345);
  std::uniform_int_distribution<int> rand_dist(0, 99);
  std::cout << rand_dist(rand_src) << std::endl;
  std::cout << rand_dist(rand_src) << std::endl;
  return 0;
}

上のように、分布を関数として使うときは、引数に乱数源への参照を渡す。内部で乱数源が(必要に応じて複数回)呼ばれている。

上のソースコードでは、MTで生成される擬似乱数列をもとに、一様分布に従う0以上99以下の整数を2つ生成している。

よく使う分布:

• 離散一様分布 uniform_int_distribution
  • テンプレート引数 : 戻り値の型(int等)
  • コンストラクタの引数 : a以上b以下の乱数を生成
• 連続一様分布 uniform_real_distribution
  • テンプレート引数 : 戻り値の型(double等)
  • コンストラクタの引数 : a以上b未満の乱数を生成
• 正規分布 normal_distribution
  • テンプレート引数 : 戻り値の型(double等)
  • コンストラクタの引数 : 平均meanで標準偏差stddev (省略すると標準正規分布)

暗号論的擬似乱数

たぶんこのライブラリには無い。

分布と擬似乱数生成器を合体させる

分布に毎回擬似乱数生成器をつけるのは面倒であるから、<functional>ヘッダにあるbindとrefを使って以下のようにする。

#include <random>
#include <iostream>
#include <functional>

int main() {
  std::mt19937 rand_src(12345);
  std::uniform_int_distribution<int> rand_dist(0, 9);
  auto rand_dist_bound = std::bind(rand_dist, std::ref(rand_src));
  std::cout << rand_dist_bound() << std::endl;
  std::cout << rand_dist_bound() << std::endl;
  return 0;
}

refを使わずに、

  auto rand_dist_bound = std::bind(rand_dist, rand_src);

としても一応動作するが、これは擬似乱数生成器のコピーを作成してしまうので意味が変わる。同じ擬似乱数生成器を複数の分布で使う場合は注意が必要(通常、refをつけるほうが好ましい)

これは以下のようにしても同じことである:

#include <random>
#include <iostream>
#include <functional>

int main() {
  std::mt19937 rand_src(12345);
  auto rand_dist_bound = std::bind(
    std::uniform_int_distribution<int>(0, 9),
    std::ref(rand_src));
  std::cout << rand_dist_bound() << std::endl;
  std::cout << rand_dist_bound() << std::endl;
  return 0;
}

さらに、この擬似乱数生成器はこの分布でしか使わないというのであれば、以下のようにもできる(この場合はrefは使わない):

#include <random>
#include <iostream>
#include <functional>

int main() {
  auto rand_dist_bound = std::bind(
    std::uniform_int_distribution<int>(0, 9),
    std::mt19937(12345));
  std::cout << rand_dist_bound() << std::endl;
  std::cout << rand_dist_bound() << std::endl;
  return 0;
}

シードの決め方

シードの決め方は場合による。大雑把に言うと次の2種類:

• 外部からの乱数に基づいて決める
• 決め打ち

ただし、以下のことに注意が必要だ:

• 外部からの乱数が必要な状況はあまり多くない : 乱数に基づくアルゴリズムは、シード決め打ちの擬似乱数で問題なく動作する。
• むしろ、再現性を考えると、シードを決め打ちにしたほうが良い。
• 「実行ごとに動作を変えたい」という需要は、コマンドライン引数などでシードを指定できるようにするだけで満足されることがある。

外部からの乱数に基づいてシードを決める

外部からの乱数に基づいてシードを決めるには、単に以下のようにすればよい:

#include <random>
#include <iostream>

int main() {
  std::random_device rand_dev;
  std::mt19937 rand_src(rand_dev());
  std::cout << rand_src() << std::endl;
  std::cout << rand_src() << std::endl;
  return 0;
}

このようにすると、毎回シードが変わるので、実行するごとに異なる整数が表示される。

外部からの乱数源を1回しか使っていないので、以下のようにもできる:

#include <random>
#include <iostream>

int main() {
  std::mt19937 rand_src(std::random_device{}());
  std::cout << rand_src() << std::endl;
  std::cout << rand_src() << std::endl;
  return 0;
}

コマンドライン引数に基づいてシードを決める

例えば、コマンドライン引数の1番目がある場合はそれをシードとして使うようにするには:

#include <random>
#include <iostream>
#include <string>

int main(int argc, char *argv[]) {
  int seed = 12345;
  if(argc > 1) {
    seed = std::stoi(argv[1]);
  }
  std::mt19937 rand_src(seed);
  std::cout << rand_src() << std::endl;
  std::cout << rand_src() << std::endl;
  return 0;
}

また、コマンドライン引数を与えない場合のデフォルトは、外部からの乱数でもよいかもしれない:

#include <random>
#include <iostream>
#include <string>

int main(int argc, char *argv[]) {
  int seed;
  if(argc > 1) {
    seed = std::stoi(argv[1]);
  } else {
    seed = std::random_device{}();
  }
  std::mt19937 rand_src(seed);
  std::cout << rand_src() << std::endl;
  std::cout << rand_src() << std::endl;
  return 0;
}

サンプルコード

POSIX usleep(3)を使って、1秒間あたり平均5個のランダムな(ポアソン過程に基づく)イベントを発生させる (十分たくさんの粒子があるときの放射線の発生とかがこれ)

#include <random>
#include <iostream>
#include <string>
#include <functional>
#include <unistd.h>

int main(int argc, char *argv[]) {
  int seed;
  if(argc > 1) {
    seed = std::stoi(argv[1]);
  } else {
    seed = std::random_device{}();
  }
  std::mt19937 rand_src(seed);
  auto rand = std::bind(
      std::exponential_distribution<double>(5.0 / 1000000.0),
      std::ref(rand_src));
  while(true) {
    std::cout << "a" << std::flush;
    usleep(rand());
  }
  std::cout << rand_src() << std::endl;
  std::cout << rand_src() << std::endl;
  return 0;
}

いわゆる「中卒」は数学/情報オリンピックには参加できるのか否か

「高校生に相当する年齢だが、高校等の教育機関に在学していない」場合、数学オリンピックや情報オリンピックには参加できるのか、という問題がある。

該当する組織に直接訊ねるのが最も正確だと思われるが、2015/06/26時点の資料を読む限り、おそらく以下の通りだと思われる。

• 数学オリンピック・情報オリンピックともに、年齢制限がある。
• 数学オリンピック(国際・日本)は、大学等に入学していなければ参加できる。すなわち、いわゆる「中卒」でも参加できる。
• 情報オリンピック(国際・日本)は、高校等に在学していれば参加できる。すなわち、いわゆる「中卒」は参加できない。
• (JOIの予選は誰でも参加できる。)

以下、根拠となる文書を引用する。

日本数学オリンピック

2016年1月時点で大学教育（またはそれに相当する教育）を受けていない20歳未満の者。但し、IMO代表資格は、IMO大会時点で大学教育等を受けていない20歳未満の者。

http://www.imojp.org/mo2016/jmo2016/recruit.html

国際数学オリンピック

A Country’s Contestants should normally be citizens or residents of that Country, and should be selected through that Country’s national Mathematical Olympiad or equivalent selection programme. Contestants must not have formally enrolled at a university or any other equivalent post-secondary institution, and they must have been born less than twenty years before the day of the second Contest paper.

https://www.imo-official.org/documents/RegulationsIMO.pdf

以下、qnighyによる訳:

通常、各国の競技者(参加者)はその国の市民ないしは住民であるべきであり、その国の国内数学オリンピックまたはそれと同等の選抜プログラムによって選ばれた者であるべきである。競技者は、大学やそれと同等の高等教育機関に正式に入学したことのある者であってはならない。また、競技者の誕生日は、競技日のうち2日目から数えて20年前よりも後でなくてはならない。

日本情報オリンピック

1. 2016 年 2 月 14 日（日）の第 15 回日本情報オリンピック本選競技実施時点で、高等学校、高等専門学校、中学校、中等教育学校、小学校、特別支援学校に在学し、学年が高等学校２年以下（中等教育学校や高等専門学校などの在校生は高等学校２年に相当する学年以下）であること。 日本国内において学校以外の初等・中等教育機関に所属している人は個別に相談。
2. 生年月日が 1996 年 4 月 2 日以降であること。

http://www.ioi-jp.org/joi/2015/joi-2016-outline.pdf

国際情報オリンピック

A Contestant is a student who was enrolled at a school for secondary education, in the Country they are representing, during the period September to December in the year before IOI’n, and is not older than twenty years on the 1st of July of the year of IOI’n.

http://www.ioinformatics.org/rules/reg14.pdf

以下、qnighyによる訳:

競技者(参加者)とは、該当年のIOIの前年9月から12月の間に、その者が代表する国にある中等教育のための学校に在学し、かつ、該当年のIOIのある年の7月1日時点で20歳以下である生徒のことである。

(was enrolledって在学と解釈していいんだろうか。)

C言語(標準)にM_PIは無い

C言語で円周率πを使うには M_PI を使う、と経験で知っている人は多いが、あれは実はC言語の規格には含まれていない。むしろ、処理系がM_PIを定義してはいけない事情(c - Using M_PI with C89 standard - Stack Overflow)がある。

ここでは、C言語の最新規格であるC11と等価なN1570 (http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf) を参考にする。これより古いC言語の規格でも同様だと思われる。

C言語の規格では、まず「標準に準拠したプログラム」は何かということを定義し、続いて「標準に準拠した処理系」は何かということを定義する、という手順を踏んでいる。

Strictly conforming program

Strictly conforming programとは、最も移植性が高いプログラムである。あるプログラムがstrictly conformingであるかどうかは、この規格書の中で厳密に定義されている。大まかに言うと、

• 出力が不定動作に依存してはいけない。
• 出力が未定義動作に依存してはいけない。
• 出力が処理系定義の動作に依存してはいけない。
• 出力がminimum implementation limitsを超過してはいけない。(例えば、intは-32767以上32767以下の数値を表現できることは仮定してよいが、それよりも大きいとは仮定してはいけない。)

「不定動作」「未定義動作」「処理系定義の動作」「implementation limitとその最小値」なども、それぞれ厳密に定義されている。

Strictly conforming programの例

#include <stdio.h>

int main(int argc, char *argv[]) {
    printf("Hello, world!\n");
    return 0;
}

Strictly conformingではない例(mainの引数が非標準、GCC拡張であるStatements and Declarations in Expressionsを使っている)

#include <stdio.h>

int main(int argc, char *argv[], char *envp[]) {
    printf(({"Hello, world!\n";}));
    return 0;
}

(参考: N1570 p.8)

Conforming implementation

Conforming implementationとは、全てのstrictly conforming programを正しく動作させる処理系のことである。(その他、#errorでエラーになることや__cplusplusをマクロで定義しないことなど、いくつかの制約がある)

したがって、conforming implementationは、strictly conformingでないプログラムに関してはどう料理してもよい。

• Conformingだと思われる処理系の例 : gcc -std=c11 (いくつかのGCC拡張は有効だが、C標準と矛盾する機能は無効化される)
  • ただし、GCCで未実装のC11機能があるので、その点ではconformingではなさそう
• Conformingではない処理系の例 : gcc -std=gnu11

(参考: N1570 p.8)

Conforming program

あるConforming implementationが受理するプログラムはConforming programと呼ばれる。この意味では、上記のCプログラムも「正しい」Cプログラムだが、移植性は保証されない。

(参考: N1570 p.8)

識別子

次のような識別子は予約されている:

• アンダースコア+大文字、またはアンダースコア2個、で始まる識別子
• アンダースコアで始まる識別子 (ファイルスコープ、通常の名前空間とタグ名前空間のみ制限)
• 規格書内で定義されているマクロ名
• 規格書内で定義されている外部リンク名とerrno (外部リンク名としての使用のみ制限)
• 規格書内で定義されているファイルスコープの名前 (関連するヘッダーがインクルードされている場合のみ、マクロ名としておよび同一名前空間でのファイルスコープでの使用のみ制限)

つまり、

• Strictly conforming programは、予約されている識別子を独自に定義・宣言・undefしてはいけない。
• Strictly conforming programは、予約されていない識別子は自由に使ってよい。
• Conforming implementationは、予約されていない識別子を独自に定義・宣言してはいけない。 (strictly conforming programの挙動が邪魔されるので)
• Conforming implementationは、予約されている識別子をある程度自由に使える。

例えば、ヘッダーによくある

#ifndef _HOGE_INCLUDED
#define _HOGE_INCLUDED

some_declarations

#endif

は、

• ユーザー側のプログラムとしては: アンダースコアで始まっているので、strictly conformingではない。
• ライブラリとしては: strictly conforming programが使える空間を汚していないので良い。むしろ、そうしないとstrictly conforming programの使える名前空間を汚していることになる。

(参考: N1570 p.182)

math.h

math.hは、規格で存在が要請されているヘッダーの一つである。

規格では、math.hで宣言されているべき識別子の一覧も指定されている。

例えば、

• 型 : float_t, double_t が定義されている。
• マクロ : HUGE_VAL, INFINITY, NAN(NaNが使える場合だけ), ... などが定義されている。
• 関数マクロ : fpclassifyなどのマクロが定義されている。
• 関数 : cos, sin, log, ...などの関数が宣言されている。

したがって、これらの識別子は予約されていることになる。つまり、strictly conforming programは、

• cos, sin, logなどを外部リンク名として独自に定義してはいけない。
• math.hをインクルードしている場合は、logやHUGE_VALなどの識別子を独自にマクロ名やファイルスコープでの名前として使ってはいけない。

一方、問題のM_PIはここでは言及されていない。したがってこの識別子は予約されていない。

したがって、以下のようなプログラムはstrictly conformingではない。(存在しないはずのM_PIを使っているので)

#include <math.h>
#include <stdio.h>

int main(int argc, char *argv[]) {
    printf("PI = %f\n", M_PI);
    return 0;
}

一方、以下のようなプログラムはstrictly conformingである。

#include <math.h>
#include <stdio.h>

int M_PI = 3;

int main(int argc, char *argv[]) {
    printf("PI = %d\n", M_PI);
    return 0;
}

(参考: N1570 p.231)

M_PIを定義してはいけない理由

もし、conforming implementationがmath.hでM_PIを定義していたとすると、上記のStrictly conforming program

#include <math.h>
#include <stdio.h>

int M_PI = 3;

int main(int argc, char *argv[]) {
    printf("PI = %d\n", M_PI);
    return 0;
}

が正しく動作しなければいけないという制約に反する。

したがって、conforming implementationではM_PIを定義してはいけない。

実際のコンパイラー

• gccは-std=c11のもとではM_PIを定義しない。
• gccは-std=gnu11のもとではM_PIを定義する。 (つまりこのgccはconforming implementationではない)
• VC++はM_PIを定義しないらしい。

gccについては、gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2で確認した。(参考
math.h の M_PI などは仕様外だった - Gust Notch? Diary)

_USE_MATH_DEFINES

処理系によっては、

#include <math.h>
#include <stdio.h>

int main(int argc, char *argv[]) {
    printf("PI = %f\n", M_PI);
    return 0;
}

はコンパイルできないが、

#define _USE_MATH_DEFINES
#include <math.h>
#include <stdio.h>

int main(int argc, char *argv[]) {
    printf("PI = %f\n", M_PI);
    return 0;
}

のように_USE_MATH_DEFINESを指定すると、正しく動作することがある。

これは、予約された識別子を定義している

#define _USE_MATH_DEFINES

の一行によって、このプログラムがStrictly conforming programではなくなることに由来している。したがって、

#define _USE_MATH_DEFINES
#include <math.h>
#include <stdio.h>

int M_PI = 3;

int main(int argc, char *argv[]) {
    printf("PI = %d\n", M_PI);
    return 0;
}

のように、わざわざM_PIを独自に定義して使おうという危なげなプログラムがあったとしても、これは最初の1行のせいでStrictly conformingではなくなり、処理系はこれを正しく動かす義務がなくなる。

まとめ

• 厳密には、処理系はM_PIを定義してはいけない。コンパイラーは実際にそれを上手に守っている。
• 困る

GW-450DやWN-AC433UKをRaspberry Piで使う

planexのありがたい記事を参考に作業。

環境としてはRaspbian wheezyを仮定。

おおまかな流れ : まず、下準備としてカーネルモジュールのビルドに必要な道具を揃える(既に揃えてある人はスルーしてよい)。続いて、ドライバのソースコードを取得し、必要な変更を加えてからビルド、インストールする。

前提知識

記事執筆時点ではGW-450DやWN-AC433UKはRaspberry Piではそのままでは動作せず、ドライバを自分で導入してやる必要がある。

GW-450DやWN-AC433UKはMediaTekのMT-7610Uというチップセットを用いているので、中身は基本的に同じである。ただし、USBのベンダーIDとプロダクトIDは変更されているので、これをドライバ中に記述してやる必要がある。

下準備1: カーネルビルドに用いられたGCCのバージョンを調べる

ここでは、raspberry piのデフォルトのカーネルを使う場合の下準備の例を示す。Raspbianがaptで提供しているカーネルを使用する場合はこの限りではなく、単にapt-getでヘッダーファイルが含まれるパッケージを取得すればよい。

$ cat /proc/version
Linux version 3.18.5+ (dc4@dc4-XPS3-9333) (gcc version 4.8.3 20140303 (prerelease) (crosstool-NG linaro-1.13.1+bzr2650) - Linaro GCC 2014.03) ) #746 PREEMPT Mon Feb 2 13:57:16 GMT 2015

で、gcc4.8.3が使われていることがわかったので、gcc4.8系列を使う。

ただし、Linux ARMにとってgcc4.8.0から4.8.2までは "too buggy" で、Linuxを正しくビルドできないとされている(これらのバージョンを使おうとすると、あるヘッダでエラーが出て弾かれるようになっている)ので、これは避ける必要がある。

したがって、この記事の執筆時点では、gcc-4.8.3を用いるのが正解ということになる。

下準備2: gccを入れる

本来であれば、

$ sudo apt-get install gcc-4.8

で目的のバージョンが入るのが望ましい。試しに

$ gcc-4.8 -v

で、所望のバージョンが得られていれば、この節はスキップしてよい。

gcc 4.8 on Raspberry Pi Wheezy | some wide open spaceを参考に、新しいバージョンを入れる。

/etc/apt/sources.listを編集する。nanoと書かれている部分は適宜別のエディタ(vim等)に置き換えてよい。

$ sudo nano /etc/apt/sources.list

debで始まっている行を下にコピペし、wheezyと書いてある行をjessieに直す(←これらはDebianのバージョン)

例えば、

deb http://mirrordirector.raspbian.org/raspbian/ wheezy main contrib non-free rpi
deb http://mirrordirector.raspbian.org/raspbian/ jessie main contrib non-free rpi

のように、wheezyの行とjessieの行が共存した状態にする。

続いて、優先度を設定する。

$ sudo nano /etc/apt/preferences

まだこのファイルが無ければ、新しく作成してよい。以下のように編集する。

Package: *
Pin: release n=wheezy
Pin-Priority: 900

Package: *
Pin: release n=jessie
Pin-Priority: 300

Package: *
Pin: release o=Raspbian
Pin-Priority: -10

これで、原則としてwheezyを使うが、必要に応じてjessieを使うという状態になった。

aptのデータベースを更新する。

$ sudo apt-get update

jessieに入っているほうのgcc-4.8をインストールする。

$ sudo apt-get install gcc-4.8/jessie

とすれば良さそうだが、依存関係が壊れると言われるので、必要な依存関係を全て明示してinstallする。例えば、

$ sudo apt-get install gcc-4.8/jessie libmpfr4/jessie cpp-4.8/jessie libgcc-4.8-dev/jessie libgcc1/jessie libc6-dev/jessie libc-dev-bin/jessie libc6/jessie

とする。

念のため、gcc-4.8の依存関係のために書いたやつは自動でインストールしたとマークしておく。

$ sudo apt-mark auto libmpfr4 cpp-4.8 libgcc-4.8-dev libgcc1 libc6-dev libc-dev-bin libc6

下準備3: gccの特定バージョンをデフォルトにする

gccはalternativesに入っていないので、自分で追加する。

例えば、gcc-4.6, gcc-4.8が入っているときは、

$ sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.6 20
$ sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.8 50

のようにする。すると、gcc-4.8が優先度50で最大なのでデフォルトになる。

優先度に関わらず特定のバージョンをデフォルトにしたいときは、

$ sudo update-alternatives --config gcc

で所望のものを選択する。

$ gcc -v

で、所望のバージョン(記事執筆時点では4.8.3)が得られているかどうかを確認する。

下準備4: Linuxのソースコードを取得し、ビルドする

rpi-sourceを使って、Raspberry Pi用のLinuxのソースコードを取得する。

$ sudo wget https://raw.githubusercontent.com/notro/rpi-source/master/rpi-source -O /usr/bin/rpi-source && sudo chmod +x /usr/bin/rpi-source && /usr/bin/rpi-source -q --tag-update

ncurses-devを入れておく。

$ sudo apt-get install ncurses-dev

rpi-sourceを実行する。

$ rpi-source

rpi-sourceはカーネルソースを取得して必要な部分をビルドしてくれる。

成功すると、ホームディレクトリにlinuxというフォルダができる。/lib/modulesからここへのシンボリックリンクが貼られるので、これでカーネルモジュール作成の準備が整った。

ソースコードを取得する

mt7610u_wifi_sta_v3002_dpo_20130916.tar.bz2 というファイルを取得する。

MediaTekのサイトから、Linux用のMT7610U USBドライバーを取得するか、PlanexのサイトからLinux用のGW-450Dドライバーを取得する。どちらも同じものである。

これを解凍する。

$ tar jxvf mt7610u_wifi_sta_v3002_dpo_20130916.tar.bz2
$ cd mt7610u_wifi_sta_v3002_dpo_20130916

ドライバに必要な変更を加える

パッチを用意したのでこれを当ててもよい。手動で編集するはら以下のとおり。

linuxバージョンの差異への対応

include/os/rt_linux.hの

typedef struct _OS_FS_INFO_
{
	int				fsuid;
	int				fsuid;
	mm_segment_t	fs;
} OS_FS_INFO;

を、

typedef struct _OS_FS_INFO_
{
	kuid_t				fsuid;
	kgid_t				fsuid;
	mm_segment_t	fs;
} OS_FS_INFO;

と書き換える。

ベンダーID, プロダクトIDの追加

common/rtusb_dev_id.cの

USB_DEVICE_ID rtusb_dev_id[] = {
#ifdef MT76x0
	{USB_DEVICE(0x148F,0x7610)}, /* MT7610U */
	{USB_DEVICE(0x0E8D,0x7610)}, /* MT7610U */

となっている部分に、

USB_DEVICE_ID rtusb_dev_id[] = {
#ifdef MT76x0
	{USB_DEVICE(0x2019,0xAB31)}, /* GW-450D */
	{USB_DEVICE(0x04BB,0x0951)}, /* WN-AC433UK */
	{USB_DEVICE(0x148F,0x7610)}, /* MT7610U */
	{USB_DEVICE(0x0E8D,0x7610)}, /* MT7610U */

と追記する。

WPA Supplicantの設定

os/linux/config.mkの

# Support Wpa_Supplicant
# i.e. wpa_supplicant -Dralink
HAS_WPA_SUPPLICANT=n


# Support Native WpaSupplicant for Network Manager
# i.e. wpa_supplicant -Dwext
HAS_NATIVE_WPA_SUPPLICANT_SUPPORT=n

を、

# Support Wpa_Supplicant
# i.e. wpa_supplicant -Dralink
HAS_WPA_SUPPLICANT=y


# Support Native WpaSupplicant for Network Manager
# i.e. wpa_supplicant -Dwext
HAS_NATIVE_WPA_SUPPLICANT_SUPPORT=y

に変更する。

設定の変更

conf/RT2870STA.datの

SSID=11n-AP

を

SSID=

に変更する。また、

AuthMode=OPEN
EncrypType=NONE

を

AuthMode=WPA2PSK
EncrypType=AES

に変更する。(WPA2PSK/AESを使わない場合にどうすればよいかは未調査)

なぜか、デフォルトではconf/RT2870STA.datではなくconf/RT2860STA.datをインストールするようになってしまっているので、os/linux/config.mkの640行目あたりにある

ifneq ($(or $(findstring mt7650u,$(CHIPSET)),$(findstring mt7630u,$(CHIPSET)),$(findstring mt7610u,$(CHIPSET))),)
WFLAGS += -DMT76x0 -DRT65xx -DRLT_MAC -DRLT_RF -DRTMP_MAC_USB -DRTMP_USB_SUPPORT -DRTMP_TIMER_TASK_SUPPORT -DA_BAND_SUPPORT -DRTMP_EFUSE_SUPPORT -DNEW_MBSSID_MODE -DCONFIG_ANDES_SUPPORT
#-DRTMP_FREQ_CALIBRATION_SUPPORT
#-DRX_DMA_SCATTER
ifneq ($(findstring mt7650u,$(CHIPSET)),)
WFLAGS += -DMT7650
endif

ifneq ($(findstring mt7630u,$(CHIPSET)),)
WFLAGS += -DMT7630
endif

ifneq ($(findstring mt7610u,$(CHIPSET)),)
WFLAGS += -DMT7610
endif

ifneq ($(findstring $(RT28xx_MODE),AP),)
#WFLAGS += -DSPECIFIC_BCN_BUF_SUPPORT
endif

ifeq ($(HAS_CSO_SUPPORT), y)
WFLAGS += -DCONFIG_CSO_SUPPORT -DCONFIG_TSO_SUPPORT
endif

CHIPSET_DAT = 2860
endif

を見つけ(mt7610uと書いてあるのがポイント)、この末尾の

CHIPSET_DAT = 2860

を

CHIPSET_DAT = 2870

に変更する。

ビルド＆インストール

$ make
$ sudo make install

これでインストールされる。

あとは通常の無線LANドングルと同様に使用できる。

アップデートへの対応

rpi-updateでアップデートした場合、新しいカーネルが入ってくることがある。この場合、rpi-sourceを実行して対応するヘッダーファイル等を作成し、ドライバを再度ビルド＆インストールすればよい。

Coqの新機能、Primitive Projectionについて

Coqリポジトリのtrunkを見ると、次の2つの機能が入っていることがわかります。

• Universe Polymorphism
• Primitive Projection

Universe Polymorphismは、グローバル定義をUniverseのレベルについて量化した形で定義することができる機能で、型に飾り付けをしたい場合(Homotopy n-typeやCategoryなどを定義したい場合)に宇宙ごとに異なる定義をする必要がなくなるという利点があります。

というのはさておき、この記事ではPrimitive Projectionを紹介します。

Primitive Projectionは、レコード型を定義したときにできる射影関数がプリミティブになるという機能です。Coqの内部で、普通の関数とは異なる特別な値として扱われるようです。

利点は次の2点のようです。

• 型検査の効率Up
• η変換ができる

ここでは後者の点についてサンプルコードを示します。

(* 従来のレコード型 *)
Record Foo := Build_Foo {
  foo : unit
}.

Set Primitive Projections.

(* Primitive Projectionを有効にしたレコード型 (Primitive Recordと呼ぶ) *)
Record Bar := Build_Bar {
  bar : unit
}.

(* 従来のレコード型では、η変換はできない *)
Goal forall f : Foo, f = Build_Foo (foo f).
Proof.
  Fail reflexivity.
Abort.

(* Primitive Projectionを有効にしたレコード型では、η変換ができる *)
Goal forall b : Bar, b = Build_Bar (bar b).
Proof.
  reflexivity.
Qed.


(* どうやら、射影関数を自分で定義しても、同じ結果になるらしい？ *)

Definition foo2(f:Foo) : unit :=
  let (foo2) := f in foo2.

Goal forall f : Foo, f = Build_Foo (foo2 f).
Proof.
  Fail reflexivity.
Abort.

Definition bar2(b:Bar) : unit :=
  let (bar2) := b in bar2.

Goal forall b : Bar, b = Build_Bar (bar2 b).
Proof.
  reflexivity.
Qed.

補足

そもそも、関数に関するη変換が入ったのが最近 (Coq 8.4以降) です。サンプルコードを示します。

Goal (fun (f:nat->nat) (n:nat) => f n) = (fun (f:nat->nat) => f).
Proof.
  reflexivity.
Qed.

面倒なので確かめていませんが、このような証明は以前は成立しなかったはずです。