From 5791ee6b64136ecb0a727e32997b33f4bfab2c31 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 21 Feb 2016 15:30:59 +0000 Subject: [PATCH] MaTeX - bug fixed in rendering of application: the head was not rendered sometimes - we can generate the list of the produced TeX files - TeX item for comments was missing test - bug fixed in matex.sty: pages were not ejected properly causig memory overflow - now includes the whole \lambda\delta version 1 (737 pages for now) - object numbering is now supported --- matita/components/binaries/matex/Makefile | 18 ++++--- matita/components/binaries/matex/TeX.ml | 1 + matita/components/binaries/matex/TeXOutput.ml | 1 + matita/components/binaries/matex/engine.ml | 17 +++++-- matita/components/binaries/matex/matex.ml | 10 +++- matita/components/binaries/matex/options.ml | 13 ++++- matita/components/binaries/matex/options.mli | 4 ++ matita/components/binaries/matex/test/Make | 2 + .../components/binaries/matex/test/Makefile | 5 +- .../components/binaries/matex/test/matex.sty | 23 +++++---- .../components/binaries/matex/test/test.tex | 50 ++----------------- 11 files changed, 74 insertions(+), 70 deletions(-) diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile index 42cf1c181..342ba027d 100644 --- a/matita/components/binaries/matex/Makefile +++ b/matita/components/binaries/matex/Makefile @@ -5,14 +5,20 @@ REQUIRES = helm-ng_library include ../Makefile.common +PROBE = ../probe/probe.native REGISTRY = $(RT_BASE_DIR)/matita.conf.xml +OBJS = Make.objs -OBJS = cic:/matita/lambdadelta/basic_1/pr0/pr0/pr0_confluence.con\ - cic:/matita/lambdadelta/basic_1/pr0/defs/pr0_ind.con\ - cic:/matita/lambdadelta/basic_1/pr0/defs/pr0.ind +BASEURI = cic:/matita/lambdadelta/basic_1/ -test: - @echo MaTeX: $(OBJS:cic:/matita/lambdadelta/basic_1/pr0/%=%) - $(H)./matex.native -O test -t -p $(REGISTRY) $(OBJS) +test: test/$(OBJS) + +$(OBJS): + @echo probe: $(BASEURI) + $(H)$(PROBE) $(REGISTRY) -g $(BASEURI) -os > $@ + +test/$(OBJS): $(OBJS) ./matex.native + @echo MaTeX: processing $(OBJS) + $(H)./matex.native -O test -l $(OBJS) -t -p $(REGISTRY) `cat $<` .PHONY: test diff --git a/matita/components/binaries/matex/TeX.ml b/matita/components/binaries/matex/TeX.ml index 01ab717f1..ccf2ffa6a 100644 --- a/matita/components/binaries/matex/TeX.ml +++ b/matita/components/binaries/matex/TeX.ml @@ -17,6 +17,7 @@ type item = Free of string (* free text *) | Text of string (* quoted text *) | Macro of string (* macro *) | Group of text (* group *) + | Note of string (* comment *) and text = item list (* structured text *) diff --git a/matita/components/binaries/matex/TeXOutput.ml b/matita/components/binaries/matex/TeXOutput.ml index f92101c30..f18b2b44a 100644 --- a/matita/components/binaries/matex/TeXOutput.ml +++ b/matita/components/binaries/matex/TeXOutput.ml @@ -32,6 +32,7 @@ let rec out_item och = function | T.Text s -> P.fprintf och "%s" (X.fold_string quote "" s) | T.Macro s -> P.fprintf och "\\%s%%\n" s | T.Group t -> P.fprintf och "{%a}%%\n" out_text t + | T.Note s -> P.fprintf och "%% %s\n" s (* interface functions ******************************************************) diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index 5a1a3e345..165986b47 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -141,8 +141,8 @@ let rec proc_proof st ris c t = match t with let is_w = proc_term [] c w in let ris = mk_open st ris in proc_proof (next st) (mk_dec "PRIM" is_w s ris) (K.add_dec s w c) t - | C.Appl ts -> - let rts = X.rev_neg_filter (A.not_prop2 c) [] ts in + | C.Appl (t0 :: ts) -> + let rts = X.rev_neg_filter (A.not_prop2 c) [t0] ts in let ris = T.Macro "STEP" :: mk_inferred st c t ris in let tts = L.rev_map (proc_term [] c) rts in mk_exit st (T.rev_mk_args tts ris) @@ -174,17 +174,24 @@ let proc_proof rs c t = try proc_proof (init ()) rs c t with (* top level processing *) +let note = T.Note "This file was automatically generated by MaTeX: do not edit" + let proc_item item s t = let is = [T.Macro "end"; T.arg item] in - T.Macro "begin" :: T.arg item :: T.arg s :: T.free s :: proc_term is [] t + note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free s :: proc_term is [] t let proc_top_proof s t = let tt = A.process_top_term s t in (* anticipation *) - let ris = [T.free s; T.arg s; T.arg "proof"; T.Macro "begin"] in + let ris = [T.free s; T.arg s; T.arg "proof"; T.Macro "begin"; note] in L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof ris [] tt) let open_out_tex s = - open_out (F.concat !G.out_dir (s ^ T.file_ext)) + let fname = s ^ T.file_ext in + begin match !G.list_och with + | None -> () + | Some och -> P.fprintf och "%s\n" fname + end; + open_out (F.concat !G.out_dir fname) let proc_pair s ss u = function | None -> diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml index 59460ce4a..7e296aa03 100644 --- a/matita/components/binaries/matex/matex.ml +++ b/matita/components/binaries/matex/matex.ml @@ -24,6 +24,7 @@ module K = Kernel let help_O = " Set this output directory" let help_X = " Clear configuration and options" +let help_l = " Output the list of generated files in this file" let help_p = " omit types (default: no)" let help_t = " Test anticipation (default: no)" @@ -47,6 +48,10 @@ let no_init () = let malformed s = failwith ("MaTeX: main: malformed argument: " ^ s) +let set_list fname = + let file = F.concat !G.out_dir fname in + G.close_list (); G.list_och := Some (open_out file) + let process s = if is_registry s then init s else if !G.no_init then no_init () @@ -54,12 +59,15 @@ let process s = else malformed s let main = -try +begin try A.parse [ "-O", A.String ((:=) G.out_dir), help_O; "-X", A.Unit G.clear, help_X; + "-l", A.String set_list, help_l; "-p", A.Set G.no_types, help_p; "-t", A.Set G.test, help_t; ] process help with | X.Error s -> X.log s +end; +G.close_list () diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml index 14dc4e2c9..ba1f39849 100644 --- a/matita/components/binaries/matex/options.ml +++ b/matita/components/binaries/matex/options.ml @@ -26,6 +26,8 @@ let default_test = false let default_no_types = false +let default_list_och = None + (* interface ****************************************************************) let status = new P.status @@ -40,10 +42,17 @@ let test = ref default_test (* test anticipation *) let no_types = ref default_no_types (* omit types *) +let list_och = ref default_list_och (* output stream for list file *) + +let close_list () = match !list_och with + | None -> () + | Some och -> close_out och + let clear () = - R.clear (); + R.clear (); close_list (); no_init := default_no_init; out_dir := default_out_dir; proc_id := default_proc_id; test := default_test; - no_types := default_no_types + no_types := default_no_types; + list_och := default_list_och diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli index 2c0e9b9b6..4629423c5 100644 --- a/matita/components/binaries/matex/options.mli +++ b/matita/components/binaries/matex/options.mli @@ -21,4 +21,8 @@ val test: bool ref val no_types: bool ref +val list_och: out_channel option ref + val clear: unit -> unit + +val close_list: unit -> unit diff --git a/matita/components/binaries/matex/test/Make b/matita/components/binaries/matex/test/Make index e69de29bb..14c1cbe22 100644 --- a/matita/components/binaries/matex/test/Make +++ b/matita/components/binaries/matex/test/Make @@ -0,0 +1,2 @@ +matex.sty +objs.tex diff --git a/matita/components/binaries/matex/test/Makefile b/matita/components/binaries/matex/test/Makefile index 703cbc8fb..00db5d193 100644 --- a/matita/components/binaries/matex/test/Makefile +++ b/matita/components/binaries/matex/test/Makefile @@ -6,7 +6,7 @@ UNLOG = ./unlog.pl MAIN = test -SOURCES = $(shell cat Make) matex.sty +SOURCES = $(shell cat Make) $(shell cat Make.objs) all: $(MAIN).dvi @@ -36,3 +36,6 @@ $(MAIN).pdf: $(MAIN).ps $(MAIN).tar: $(MAIN).log $(UNLOG) $< $@ + +objs.tex: + @sed "s/\(.*\).tex/\\\\input{\1}/" Make.objs > $@ diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty index a37b00545..a889be7ad 100644 --- a/matita/components/binaries/matex/test/matex.sty +++ b/matita/components/binaries/matex/test/matex.sty @@ -1,5 +1,5 @@ \NeedsTeXFormat{LaTeX2e}[1995/12/01] -\ProvidesPackage{matex}[2016/02/15 MaTeX Package] +\ProvidesPackage{matex}[2016/02/21 MaTeX Package] \RequirePackage{xcolor} \ExecuteOptions{} \ProcessOptions* @@ -17,20 +17,23 @@ \newcommand*\ma@qed{ma@blue} \newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}} +\newcommand*\neverindent{\setlength\parindent{0pt}} \newcommand*\ObjLabel[1]{\label{obj:#1}} \newcommand*\ObjRef[1]{\ref{obj:#1}} +\newcommand*\ObjIncNode{} +\newcommand*\ObjNode{} \newcommand*\ma@setlabel[2]{\setlabel{#1}\ObjLabel{#2}} -\newcommand*\ma@thehead[2]{\textbf{#1 (#2)}\\} -\newcommand*\ma@theneck[1]{\textsl{#1}\\} +\newcommand*\ma@thehead[2]{\ObjIncNode\textbf{#1 \ObjNode(#2)}\neverindent\par} +\newcommand*\ma@theneck[1]{\textsl{#1}\neverindent\par} -\newenvironment{axiom}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Axiom}{#1}}{} -\newenvironment{declaration}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Declaration}{#1}}{} -\newenvironment{definition}[2]{}{} -\newenvironment{proposition}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Proposition}{#1}}{} -\newenvironment{proof}[2]{\ma@theneck{Proof}}{} -\newenvironment{ma@step}[1]{\color{#1}}{\\} +\newenvironment{axiom}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Axiom}{#1}}{\par} +\newenvironment{declaration}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Declaration}{#1}}{\par} +\newenvironment{definition}[2]{}{\par} +\newenvironment{proposition}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Proposition}{#1}}{\par} +\newenvironment{proof}[2]{\ma@theneck{Proof}}{\par} +\newenvironment{ma@step}[1]{\color{#1}}{\par} \newcommand*\ma@tmp{} \newcommand*\ma@skip[4]{} @@ -63,7 +66,7 @@ \newcommand*\EXIT[1]{\ma@head{}{}{\ma@exit}{end} of block #1\ma@stop} \newcommand*\OPEN[3]{\ma@head{}{}{\ma@open}{#1} is this block #3\ma@stop} \newcommand*\PRIM[3]{\ma@head{}{}{\ma@prim}{#1} will have type #3\ma@stop} -\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{\ma@fwd}{#1} has type #3\\} +\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{\ma@fwd}{#1} has type #3\par} \newcommand*\BODY[1]{being #1\ma@stop} \newcommand*\STEP[1]{by #1\ma@tail} \newcommand*\DEST[1]{by cases on #1\ma@tail} diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex index 057a1f54b..a85f8c8f6 100644 --- a/matita/components/binaries/matex/test/test.tex +++ b/matita/components/binaries/matex/test/test.tex @@ -4,53 +4,13 @@ \usepackage[american]{babel} \usepackage{matex} -\begin{document} - -\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_beta.type} - -\bigskip - -\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_comp.type} - -\bigskip - -\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_delta.type} - -\bigskip - -\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_refl.type} - -\bigskip - -\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_tau.type} - -\bigskip - -\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0.type} +\newcounter{node} +\renewcommand*\ObjIncNode{\stepcounter{node}} +\renewcommand*\ObjNode{\arabic{node} } -\bigskip - -\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_upsilon.type} - -\bigskip - -\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_zeta.type} - -\bigskip - -\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.type} - -\bigskip - -\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.body} - -\bigskip - -\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.type} - -\bigskip +\begin{document} -\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body} +\input{objs} \bigskip -- 2.39.2