問題タブ [proof-general]

この質問は、Emacs の Proof General 内で Coq モードを設定することに関するものです。

Emacs に Coq のキーワードと表記を対応する Unicode グリフに自動的に置き換えさせようとしています。funギリシャ語の小文字のラムダ λ や、全称量化記号 ∀ などを定義forallすることができました。単語の記号を定義するのに問題はありませんでした。

問題は、演算子=>、->、<->などを Unicode シンボル ⇒→↔ に定義しようとすると、Coq の対応する Unicode グリフに置き換えられないことです。ただし、*scratch*テストすると、バッファ内で置き換えられます。同じメカニズムを使用して、Unicode グリプを Coq 表記と一致させています。

問題は、Coq モードが特定の句読点を特別なものとしてマークするため、Emacs が私のコードを無視してそれらを Unicode グリフに置き換えることにあると思われますが、よくわかりません。誰かが私のためにこれに光を当てることができますか?

編集 4 : これは、実際には一般的な TTY 入力の制限にすぎないことがわかりました。問題の原因となっている OCaml、Coq、または Emacs については特に何もありません。

Emacs で Proof General を使用して Coq プログラムに取り組んでいますが、入力が長すぎるバグを発見しました。Proof Generalを介して送信する領域にcoqtop1023 文字を超える文字が含まれている場合、Proof General (Emacs ではありません) は応答を待っている間にハングし、*coq*バッファーには^G1023 文字を超える文字ごとに 1 つの余分な文字が含まれます。たとえば、1025 文字の場合region が に送信されたcoqtop場合、*coq*バッファは 2 つの余分な文字で終了し^G^Gます。ファイルのこのポイントを超えて先に進むことができず、coqtopプロセスを強制終了する必要があります (C-c C-xまたはターミナルからkill/を使用killall)。

この制限に関する何かは、coqtopそれ自体から生じます。1024文字以上の文字列を生成し、それをパイプする場合

その後、すべて正常に動作します。(同様に、正常にcoqc動作します。) しかし、ターミナルで実行するcoqtopと、1 行に 1024 文字を超える文字を入力できません。これには、最後の改行文字が含まれます。したがって、1023 文字の行を入力してから改行を押すと機能します。しかし、1024 文字を入力した後、return を含む (delete などは含まない) 任意のキーを押しても、ビープ音が鳴るだけです。そして、ocaml(OCaml トップレベル) が同じ動作をすることがわかりました:

ocaml正常に動作しますが、端末から実行している場合、1 行に 1024 文字を超える文字を入力できません。私の理解ではcoqtop、OCaml のトップレベルに依存しているため (より明らかに as として実行した場合coqtop -byte)、これは関連する制限であると思います。

関連するソフトウェア バージョンは次のとおりです。

• HomebrewのOCaml 3.12.1 ;
• HomebrewのCoq 8.3pl3 (および 8.3pl2) ;
• 証明 一般4.1;
• Emacs for Mac OS XからのGNU Emacs 24.1.1のビルド。と
• Mac OS X 10.6.7。

そして私の質問は次のとおりです。

• この文字数制限の実施ocamlについてはどうですか? coqtopそして、なぜパイプやファイルからの入力ではなく、端末や Emacs からの入力だけなのですか?
• Proof General がこの制限を (明らかに) 無知であるために、エラーがハングしたり、謎^Gの s が発生したりするのはなぜですか?
• この制限を回避するにはどうすればよいですか? 私の最終目標は、Proof General/Emacs 内で Coq を使用することなので、根本的な問題を回避する回避策は問題ありません。

編集 3: 1024 文字の入力制限が Ocaml トップレベルにも存在することを発見した後 (関連していると思われるもの)、その情報を追加し、元の問題の説明を削除しました。(必要に応じて編集履歴を参照してください)。

私はいくつかの正規表現をいじっていますが、いくつかの一致を見ているうちに、なぜ exec 関数が同じ数の結果を生成したのかが気になりました。

正規表現がn 個の結果を返す理由を単に受け入れるのではなく、より快適に感じることができるように、操作の内部動作について少し説明を求めているだけです。

元。

上記の例では、「Zip or City & State」に一致する理由はわかりますが、未定義の値で 2 番目の一致が生成される理由はわかりません。

前もって感謝します。

Aquamacs の Emacs で Proof General を使用しており、ピリオド (".") を書き込むたびにすべてが実行されます (そのピリオドまで)。電気的な動作のように見えますが、そうではありません。他のすべてのキーは正常に動作します。

これは、誤ってキーバインディングを使用したときに開始されたモードであることを知っています。セッションを再開すると効果は停止しますが、停止する (または開始する) ためのキーバインドを知りたいです。

このモードが何と呼ばれているか知っていますか？オンラインでも見つかりません。

私はIsabelleとProof Generalの両方の初心者です。

Isabelle で使用するために Proof General で暗いテーマを設定しようとしていますが、選択したテーマ (例: tango-dark、ample、monokaiなど) に関係なく、変更されていない内部構文が非常に読みにくい緑色で強調表示されます。テーマのカスタマイズを検討しましたが、カスタマイズする場所がわかりません。以下は のスクリーンショットですtango-dark。

Isabelle でうまく機能する既存のナイス ダーク テーマはありますか、または Proof General で Isabelle の内部構文の強調表示をカスタマイズするにはどうすればよいですか?

この問題は、Proof General を実行しているときにのみ発生します。これは、Proof General によって開始されたランダムなマイナー モードであると想定していますが、どのモードかはわかりません! 名前を認識できる場合に備えて、以下にマイナーモードのリストを含めます。

Emacs でピリオドを配置すると、次のようにカーソルがピリオドの前にジャンプします。

何かを書いている|

何かを書いています。|

何かを書いています|。

where|はカーソルを表し、最後の 2 行はすぐに次々と発生します。

ピリオドのある行の終わりをクリックすると、同じことが起こります。カーソルはピリオドの後に表示され、ピリオドの直前にジャンプします。

いくつかの文。（ここをクリック）

いくつかの文。| |

いくつかの文|。

最後の 2 行が次々と発生します。

名前を見つけることができる場合に備えて、マイナーモードのリストを次に示します。

ほとんどの IDE またはテキスト エディターでは、用語を右クリックすると、その用語が定義されているファイルに移動できます。CoqIDE にはそれがないようなので、私は を実行coqdoc myfile.v --htmlしてから、生成された HTML ドキュメントに移動しました。しかし、そのファイルでクリックできる用語は、Coq 標準ライブラリに関するものだけです。ssreflect で定義された用語 (たとえば) はクリックできません。

Coqファイルで、用語/識別子が定義されている場所(およびそのソースコード)をすばやく検索できる標準的な方法はありますか? CoqIDE または emacs + ProofGeneral (私は CoqIDE を使用していますが、emacs/ProofGeneral にこの機能があれば切り替えます)。

それとも、使用するすべての Coq プロジェクトと依存関係のドキュメントを生成する標準的な方法ですか?