prooftree - Dalam Talian di Awan

JADUAL:

NAMA

prooftree - paparan proof-tree untuk Proof General

SINOPSIS

prooftree [Pilihan...]

DESCRIPTION

prooftree menggambarkan pokok bukti semasa pembangunan bukti dengan Bukti Umum. Pada masa ini
ia hanya berfungsi untuk ayam jantan, walaupun menambah sokongan untuk pembantu bukti lain sepatutnya
agak mudah.

Untuk memulakan paparan pokok bukti, tekan butang prooftree ikon dalam Bukti Umum bar alat atau
pilih entri menu Pembuktian Umum -> Mula / Berhenti prooftree atau taip Sk Cd (yang berjalan
proof-tree-luaran-paparan-togol). Di dalam bukti, ini akan segera memulakan pembuktian-
paparan pokok untuk bukti semasa. Di luar bukti, Bukti Umum ingat untuk memulakan
paparan pokok bukti untuk bukti seterusnya.

Dalam keadaan biasa prooftree dimulakan oleh Bukti Umum sebagai Emacs subproses.
Pengguna berinteraksi dengan prooftree hanya melalui antara muka pengguna grafik. A substansial
sebahagian daripada tugas visualisasi pokok bukti dilakukan oleh Bukti Umum. Oleh itu bukan sahaja
yang prooftree argumen baris arahan tetapi juga aspek lain hanya boleh dikonfigurasikan di dalam
Bukti Umum, Lihat Bukti Umum Penyesuaian di bawah.

PILIHAN

-bantu Cetak sinopsis dan keluar.

-config
Buka dialog konfigurasi semasa permulaan (jika anda ingin menukar konfigurasi
tanpa bermula Bukti Umum).

-geometri spec
Menetapkan geometri X tetingkap utama. spec ialah rentetan geometri X standard dalam
borang xposxypos[+xoff[+yoff]].

-tee fail
Tulis semua input ke fail (biasanya untuk tujuan penyahpepijatan).

-debug Berikan butiran lanjut tentang ralat.

-dialog-bantuan
Buka dialog bantuan semasa permulaan. Terutamanya berguna untuk membaca pruf teks bantuan.

UTAMA BUKTI DISPLAY

prooftree membuka satu tetingkap untuk setiap bukti yang diminta untuk dipaparkan. tingkap ini
mengandungi graf pokok bukti dan paparan kecil untuk urutan dan arahan bukti.

Warna
Cawangan dalam graf pokok bukti diwarnakan mengikut keadaannya. prooftree
membezakan antara negeri berikut.

semasa (biru secara lalai)
Cawangan semasa ialah dahan daripada akar pokok bukti kepada arus
Matlamat.

tidak terbukti (warna latar depan lalai)
Cawangan tidak terbukti jika ia mengandungi matlamat bukti terbuka.

terbukti tidak lengkap (cyan secara lalai)
Cawangan yang tidak dibuktikan dengan lengkap mempunyai pembuktiannya, tetapi sebahagian daripadanya wujud
pembolehubah yang telah diperkenalkan dalam cawangan ini belum (belum) instantiated.

terbukti sebahagiannya (hijau gelap secara lalai)
Dalam cawangan yang sebahagiannya terbukti semua pembolehubah kewujudan cawangan itu sendiri adalah
instantiated, tetapi sesetengah instantiation tersebut mengandungi pembolehubah wujud yang
belum (belum) segera.

terbukti lengkap (hijau secara lalai)
Sesuatu cawangan dibuktikan lengkap jika semua pembolehubah kewujudannya dicontohkan
istilah yang sendiri tidak mengandungi sebarang pembolehubah wujud.

ditipu (merah secara lalai)
Cawangan yang ditipu mengandungi perintah bukti penipuan, seperti mengaku

Warna serta banyak lagi prooftree parameter boleh diubah dalam prooftree
konfigurasi Dialog (lihat di bawah).

navigation
Apabila pokok bukti tumbuh besar seseorang boleh mengemudi dengan pelbagai cara. Sebagai tambahan kepada
bar skrol dan kekunci biasa seseorang boleh menggerakkan pokok bukti dengan menyeret dengan butang tetikus 1
ditekan. Secara lalai, menyeret menggerakkan port pandangan (iaitu, pokok bukti di bawahnya bergerak masuk
arah bertentangan). Selepas menetapkan nilai negatif untuk Seret pecutan dalam
prooftree konfigurasi Dialog, menyeret akan mengalihkan pokok bukti sebaliknya (iaitu, bukti
pokok bergerak ke arah yang sama dengan tetikus).

Sequence paparan
Paparan jujukan di bawah pokok bukti biasanya menunjukkan jujukan nenek moyang bagi
matlamat semasa. Dengan satu klik tetikus kiri seseorang boleh memaparkan sebarang arahan matlamat atau bukti masuk
paparan berturutan. Satu klik di luar pepohon bukti akan bertukar kembali kepada lalai
tingkah laku. Saiz awal paparan jujukan boleh ditetapkan dalam prooftree
konfigurasi Dialog. Nilai 0 menyembunyikan paparan jujukan.

Alat Tips
Perintah dan urutan bukti yang disingkat ditunjukkan sepenuhnya sebagai petua alat apabila tetikus
penunjuk terletak di atas mereka. Kedua-duanya, petua alat untuk arahan bukti yang disingkatkan dan untuk
jujukan boleh dimatikan secara bebas dalam prooftree konfigurasi Dialog. Yang
panjang di mana perintah bukti disingkatkan boleh dikonfigurasikan juga.

Tambahan memaparkan
Klik dua kali atau klik anjakan memaparkan sebarang arahan matlamat atau bukti dalam tambahan
tingkap. Tetingkap tambahan ini dipadamkan apabila tetingkap pokok bukti utama hilang,
kecuali mereka Sticky butang ditekan.

Eksistensial Pembolehubah
prooftree menjejaki pembolehubah kewujudan, sama ada ia telah dijadikan instantiated dan
sama ada mereka bergantung kepada yang lain, tidak (belum) wujud kewujudan. Ia menggunakan berbeza
warna untuk cawangan terbukti yang mengandungi pembolehubah kewujudan bukan instan dan
cawangan yang hanya bergantung pada beberapa kewujudan yang tidak instantiated. Senarai pada masa ini tidak
(namun) pembolehubah kewujudan instantiated dilampirkan pada perintah bukti dan jujukan masuk
petua alat dan paparan lain.

. Eksistensial Pembolehubah Dialog memaparkan jadual dengan semua pembolehubah kewujudan
bukti semasa dan kebergantungan mereka. Setiap baris jadual mengandungi butang yang menandakan
arahan bukti yang memperkenalkan pembolehubah ini (dengan latar belakang kuning, secara lalai) dan,
jika ada, perintah bukti yang membuat instantiated pembolehubah ini (dengan latar belakang oren, oleh
lalai).

Utama Menu
. Menu butang memaparkan menu utama. The Klon item mengklonkan pokok bukti semasa dalam an
tetingkap tambahan. Tetingkap tambahan ini terus memaparkan syot kilat yang diklon
pokok bukti, tidak kira apa yang berlaku dengan bukti asal.

. Tunjuk semasa item mengalihkan port pandangan ke pokok bukti supaya bukti semasa
matlamat (jika ada) akan kelihatan.

. Keluar item tamat prooftree dan menutup semua paparan pokok bukti.

Baki tiga item memaparkan, masing-masing, prooftree konfigurasi Dialog, dan
yang Bantuan and Mengenai Kami tingkap.

Konteks Menu
Satu klik kanan memaparkan Konteks Menu, yang mengandungi item tambahan.

Barang itu Buat asal kepada titik aktif di atas nod jujukan dalam pokok bukti. Kemudian ia menghantar satu
tarik balik atau buat asal permintaan kepada Proof General yang menarik balik penimbal skrip sehingga itu
berurutan.

barang-barang Memasukkan arahan and Memasukkan subproof aktif atas perintah bukti. Mereka menghantar,
masing-masing, perintah bukti yang dipilih atau semua perintah bukti dalam subpokok yang dipilih, kepada
Bukti Umum, yang memasukkannya pada titik.

CONFIGURATION

prooftree konfigurasi Dialog
Perubahan dalam dialog konfigurasi hanya berkuat kuasa apabila Memohon or OK butang adalah
ditekan. The Jimat butang menyimpan konfigurasi semasa (sebagai marshaled OCaml rekod) dalam
~/.prooftree, yang akan menimpa konfigurasi lalai terbina dalam untuk yang berikut
prooftree berlari. The Simpan semula butang dimuatkan dan menggunakan konfigurasi yang disimpan.

Bukti Umum Penyesuaian
Lokasi prooftree boleh laku dan argumen baris arahan berada dalam
kumpulan penyesuaian pokok bukti. Nyatakan perkara tertentu, seperti ungkapan biasa
untuk arahan navigasi dan menipu berada dalam kumpulan penyesuaian proof-tree-internals.
Untuk melawat kumpulan penyesuaian, taip Mx menyesuaikan-kumpulan diikuti dengan nama
kumpulan penyesuaian di dalam Bukti Umum.

HADAH

Untuk ayam jantan, bukti mesti dimulakan dengan arahan Bukti, iaitu amalan yang disyorkan
bagaimanapun (lihat laporan masalah Coq 2776).

PRASUITAS

Versi prooftree memerlukan ayam jantan 8.4beta atau lebih baik dan Bukti Umum 4.3pra130327 atau
lebih baik.

Gunakan prooftree dalam talian menggunakan perkhidmatan onworks.net