Persiapan dokumen Isabelle

Saya ingin mendapatkan kode LaTeX yang terkait dengan teori ini . Jawaban sebelumnya hanya menyediakan link ke dokumentasi. Izinkan saya menjelaskan apa yang saya lakukan.

Saya pergi ke direktori Hales.thy dan mengeksekusi isabelle mkroot, diikuti oleh isabelle build -D ., yang menghasilkan file bernama dokumen dan file *.pdf yang mencurigakan (hampir) kosong. Modifikasi perintah ini dengan menambahkan Hales.thy sebagai parameter tidak berhasil.

Saya akan sangat menghargai jika seseorang dapat menjelaskan secara singkat perintah yang diperlukan.


latex isabelle
person Rodrigo    schedule 10.08.2019    source sumber

Jawaban (1)


arrow_upward
6
arrow_downward

  1. Sebagai tindakan pencegahan, salin file Hales.thy ke direktori baru yang tidak berisi file lain dan jalankan isabelle mkroot lagi.
  2. Jika saya memahaminya dengan benar, teori Anda mengandung sorry. Dalam hal ini, agar build berhasil, Anda perlu mengaktifkan mode quick_and_dirty. Untuk ini, sebelum kemunculan pertama sorry di file teori Anda, Anda perlu memasukkan declare [[quick_and_dirty=true]].
  3. Teori Anda berisi teks mentah yang formatnya tidak sesuai. Coba ganti baris yang relevan dengan yang berikut: text‹The case \<^text>‹t^2 = 1› corresponds to a product of intersecting lines which cannot be a group› dan text‹The case \<^text>‹t = 0› corresponds to a circle which has been treated before›.
  4. Setelah ini selesai, Anda seharusnya dapat menggunakan file ROOT pada lampiran di bawah. Seperti yang Anda lihat, saya telah menentukan file teori secara eksplisit dan juga menambahkan sesi impor yang relevan.

Lampiran

session Hales = HOL +
  options [document = pdf, document_output = "output"]
sessions
  "HOL-Library"
  "HOL-Algebra"
theories
  "Hales"
document_files
  "root.tex"
person user9716869    schedule 10.08.2019
comment
Spesifikasi perintah LaTeX yang diperkenalkan oleh Isabelle selama proses pembuatan harus tersebar di sekitar file *.sty relevan yang dibuat secara otomatis. Apakah Anda melihat file seperti isabelle.sty dan isabellesym.sty di direktori yang sama dengan Hales.tex? Jika ya, asalkan disertakan menggunakan \usepackage, LaTeX akan mengenalinya. Saya ingin tahu apa sebenarnya yang Anda coba lakukan... Apakah Anda mengalami masalah dengan proses pembangunan setelah mengikuti 1-4? - person user9716869; 11.08.2019
comment
Ngomong-ngomong, jika itu masuk akal bagi Anda, saya ingin mengucapkan terima kasih atas bantuan Anda di bagian yang saya tulis sebagai bukti, tapi saya memerlukan nama aslinya... - person Rodrigo; 25.11.2019
comment
Terima kasih. Seperti yang saya sebutkan sebelumnya, saya tidak mencari atribusi apa pun. Anda dapat memberikan tautan ke postingan yang relevan di SO di komentar di kode jika Anda mau. Namun, menurut saya, file tersebut tidak boleh muncul dalam dokumen bukti formal (yaitu file *.pdf yang dihasilkan). Mengenai identitas saya, sebenarnya saya tidak menyembunyikannya dari siapa pun secara khusus, hanya dari masyarakat umum. Jika Anda tertarik, silakan kirimkan email kepada saya dan tanyakan secara eksplisit dan saya akan memberikannya (Saya harus melakukan ini beberapa kali, jadi, saya rasa, saat ini, sudah cukup banyak orang yang mengetahuinya. ). - person user9716869; 25.11.2019