การเตรียมเอกสารของอิสซาเบล

ฉันต้องการรับโค้ด LaTeX ที่เกี่ยวข้องกับ ทฤษฎีนี้ . คำตอบก่อนหน้านี้มีเฉพาะลิงก์ไปยังเอกสารประกอบเท่านั้น ให้ฉันอธิบายสิ่งที่ฉันทำ

ฉันไปที่ไดเรกทอรีของ Hales.thy และดำเนินการ isabelle mkroot ตามด้วย isabelle build -D . ซึ่งสร้างไฟล์ชื่อ document และไฟล์ *.pdf ซึ่งว่างเปล่าอย่างน่าสงสัย (เกือบ) การแก้ไขคำสั่งนี้โดยการเพิ่ม Hales.thy เป็นพารามิเตอร์ไม่สำเร็จ

ฉันจะขอบคุณถ้ามีคนอธิบายคำสั่งที่จำเป็นโดยย่อ


latex isabelle
person Rodrigo    schedule 10.08.2019    source แหล่งที่มา

คำตอบ (1)


arrow_upward
6
arrow_downward

  1. เพื่อเป็นการป้องกันไว้ก่อน ให้คัดลอกไฟล์ Hales.thy ลงในไดเร็กทอรีใหม่ที่ไม่มีไฟล์อื่นๆ และรัน isabelle mkroot อีกครั้ง
  2. ถ้าฉันเข้าใจถูกต้อง ทฤษฎีของคุณประกอบด้วย sorry ในกรณีนี้ เพื่อให้การสร้างสำเร็จ คุณต้องเปิดใช้งานโหมด quick_and_dirty ในกรณีนี้ ก่อนที่ sorry จะปรากฏครั้งแรกในไฟล์ทฤษฎีของคุณ คุณจะต้องแทรก declare [[quick_and_dirty=true]]
  3. ทฤษฎีของคุณมีข้อความดิบที่มีรูปแบบไม่เหมาะสม ลองแทนที่บรรทัดที่เกี่ยวข้องด้วยบรรทัดต่อไปนี้: text‹The case \<^text>‹t^2 = 1› corresponds to a product of intersecting lines which cannot be a group› และ text‹The case \<^text>‹t = 0› corresponds to a circle which has been treated before›
  4. เมื่อเสร็จแล้ว คุณควรจะสามารถใช้ไฟล์ ROOT ในภาคผนวกด้านล่างได้ อย่างที่คุณเห็น ฉันได้ระบุไฟล์ทฤษฎีอย่างชัดเจนและเพิ่มเซสชันที่นำเข้าที่เกี่ยวข้องด้วย

ภาคผนวก

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
ข้อมูลจำเพาะของคำสั่ง LaTeX ที่ Isabelle แนะนำในระหว่างกระบวนการสร้างควรกระจัดกระจายไปตามไฟล์ *.sty ที่สร้างขึ้นอัตโนมัติที่เกี่ยวข้อง คุณเห็นไฟล์เช่น isabelle.sty และ isabellesym.sty ในไดเรกทอรีเดียวกันกับ Hales.tex หรือไม่ หากเป็นเช่นนั้น หากรวมไว้โดยใช้ \usepackage แล้ว LaTeX ก็ควรจดจำได้ ฉันอยากรู้ว่าคุณกำลังพยายามทำอะไรกันแน่... คุณประสบปัญหากับกระบวนการสร้างหลังจากทำตาม 1-4 หรือไม่? - person user9716869; 11.08.2019
comment
อย่างไรก็ตาม ถ้ามันสมเหตุสมผลสำหรับคุณ ฉันอยากจะรับทราบความช่วยเหลือของคุณในส่วนที่ฉันเขียนเกี่ยวกับหลักฐาน แต่ฉันอยากได้ชื่อจริง... - person Rodrigo; 25.11.2019
comment
ขอบคุณ ดังที่ได้กล่าวไปแล้ว ฉันไม่ได้แสวงหาแหล่งที่มาใดๆ คุณสามารถระบุลิงก์ไปยังโพสต์ที่เกี่ยวข้องใน SO ในความคิดเห็นในโค้ดได้หากต้องการ อย่างไรก็ตาม ในมุมมองของฉัน สิ่งเหล่านั้นไม่ควรปรากฏในเอกสารพิสูจน์ที่เป็นทางการ (เช่น ไฟล์ *.pdf ที่สร้างขึ้น) สำหรับตัวตนของฉัน ฉันไม่ได้ปิดบังไม่ให้ใครเห็นเป็นพิเศษ ยกเว้นจากคนทั่วไปเท่านั้น หากคุณสนใจ โปรดส่งอีเมลถึงฉันและถามอย่างชัดเจนแล้วฉันจะจัดให้ (ฉันต้องทำเช่นนี้สองสามครั้ง ดังนั้นฉันคิดว่าตอนนี้มีคนไม่กี่คนที่รู้เรื่องนี้อยู่แล้ว ). - person user9716869; 25.11.2019