Open kohlhase opened 9 years ago
We should avoid yet another (additional) configuration file. Maybe just the mmt command line syntax for "build
" (that is also used in .msl files) can be extended. I suggest for example:
build <Group/Repo> <target> [<regex>] [except <regex>]
where <target>
may be one of our current targets (like sms, stex-omdoc, latexml, pdflatex, mmt-omdoc, twelf-omdoc, tptp-twelf
) possibly with the modifiers (*, !, ?
). "except
" would be a (new) keyword (hoping that we do not need to support a file or directory named except
)
Also mws, svg, lf-scala
are build targets.
@kohlhase Do you still need this feature (after #54 has been implemented)? Would it be an option to add your above entries to the META-INF/MANIFEST.MF
file?
I am not sure, how would I do the following use case: I would like to say something like
cd ~/localmh/MathHub/MiKoMH/GenCS
lmh omdoc --update
and I have the expectation that it would build all the omdoc files that need building. But it would not recurse into the */tikz
directories. How would I do that?
It does not recurse into tikz
(this is hard-coded).
is there a way to specify that it should leave out a specific file in this? e.g. because it is not ready?
No, but would you like to add the name of such a file into another file (like META-INF/MANIFEST.MF)?
Or would you rather prefer one (or multiple) --exclude
options on the lmh (and mmt) command line?
BTW the --update
option (or mmt option --onChange
) will try to build a file only once. Only MMT's --onError
would always try to rebuild a file that previously failed to build.
would you like to add the name of such a file into another file (like META-INF/MANIFEST.MF)?
yes, the proposal here was to to a file .mmtbuild
in the local directory. but the MANIFEST is also possible.
Ok, it's implemented by https://github.com/KWARC/MMT/commit/a16796051229701c74e24a2ae56c777744bd8f71. Several regexprs (separated by blanks) may follow the colon. I've tested it with a single file. I'm not sure how matches
behaves.
documentation is at the bottom of https://github.com/KWARC/MMT/wiki/Customizing-LaTeXML-processing
The java pattern http://docs.oracle.com/javase/7/docs/api/java/util/regex/Pattern.html for your example must be written as .*bar.*.tex
(where the last .
happens to match the literal .
, but it could be escaped using \
in \.
).
Make a new ticket if also directories should be excluded.
allow to specify exceptions for directories, too
I think that the regular expressions should just match the full relative path to the file. That would be useful to me. I have committed a regular expression in ```MiKoMH/TDM/META-INF/MANIFEST.MF
I match the relative path (below source), now. Also positive build-
patterns can be given.
f23f0a950f7bf1fc21facc8357f939cfb9eba0f7
someone wanted special .ignore
files within directories to be checked. (When this becomes urgent let me know.)
I would like to have mechanism where I can specify files that should not be built (by a regexp). I imagine a
.mmtbuild
file per directory which has entries likeAnd when we have something like this, we could have other build-config targets as well.