問題タブ [proof-general]

Ubuntu 12.04 LTSにemacs 23.3.1があり、一般的な証明は4.2です。「coq ホール」モード (coq をハックするときのデフォルト) で coq ファイルを編集する場合、タブを使用できません。そうすることでエラーが発生します

間違った型引数 integer-or-marker-p nil 証明 一般

ミニバッファで。これを解決するにはどうすればよいですか?

Emacs バッファで .csv ファイルを開くたびに、Proof General が起動し (まだ起動していない場合)、ウィンドウがリセットされます。これは本当に Emacs の調子を狂わせてしまい、やめなければなりません。

Proof General を扱う私の init.el の唯一の部分は次のとおりです。

私は Isabelle 2016 の使い方を学ぼうとしています。基本的には非同期プルーフ チェックのアイデアが好きですが、Isabelle/jEdit はいくつかの理由で好きではありません。最も深刻な理由は、メモリを使いすぎることです。 （私のため）。

Isabelle 2016 で古き良き Proof General を使用できれば素晴らしいと思います。Isabelle 配布ディレクトリの下のisa-isabelle-commandファイルを指すように変数を設定しました。bin/isabelleProof General のメニューを使用して Isabelle を起動すると、Emacs がハングしC-gます*isabelle*。

Proof General が定理証明者と通信するために使用する Isabelle のコンポーネントが削除されたことを示唆する、このサイトの古い投稿を認識しています。これは、Isabelle 2016 にも (まだ) 当てはまりますか? 新しいバージョンの Isabelle で Proof General を使用するにはどうすればよいですか?

この質問は、 https ://github.com/deepmind/labまたはPython のhttps://www.tensorflow.org/の deepmind オープンソース ライブラリの使用に関する指示/提案/ヘルプを求めるものです。

私は深層学習や AI などの概念に慣れていないことを考慮してください。

質問は次のとおりです。

• 値を観察してアクションを実行する必要がある数学の問題に Deepmind または Tensorflow を使用する例はありますか?

このページ ( https://deepmind.com/blog/open-sourcing-deepmind-lab/ ) で説明されているものと同様のアプローチを使用して、観察、行動、報酬などに基づいて、いくつかの値の中から選択する学習エージェント。私はこのようなことを考えていました：

• 入力: タプルのリストのリスト (リストは各ステップで変更されます)
• アクション: 入力から値を取得します (経験に基づく)
• 報酬: 返された値が、実装している残りのアルゴリズムにとって良いか悪いかである場合、ディープ ラーニング エージェントに報酬を与えます。

その他の注意事項：

• 事前にアルゴリズムをトレーニングすることはできません

入力は次のようなものです（数字のみ）：

アイデアは、deepmind がゲームをプレイするために使用するのと同じアプローチを使用することですが、ピクセルを分析してパッド (上、下、左、右、発射、ジャンプ) を使用する代わりに、学習エージェントにいくつかの数学値を分析させ、唯一のアクションとして、それらのいずれかを選択します。

このような問題に対処するための他のアプローチやライブラリ/フレームワークはありますか?