Daniel,

I am taking the liberty of copying this to the ProofPower mailing list
as it may be of interest to other users. Perhaps you might like to
join the list and continue the discussion there.

Most interactive users of ProofPower need the online documentation
and they also want to create ProofPower documents as part of their
work. Hence, the build process assumes you want and have an
installation of TeX and LaTeX. If you want to build on a
minimal system without them, then that should be possible. I haven’t
got time to build a VM to test this in just now, but what I would try
is running configure (without pptex as you don’t want it) and then
editing the install script to change the line.

                if      ! make -f $d.mkf inst >>"$PPBUILDDIR/build.log" 2>&1

to read:

                if      ! make -f $d.mkf bininst >>"$PPBUILDDIR/build.log" 2>&1

then run install with -d, which stops it doing the last step that builds the
HTML index file in $PPHOME/doc.

Do let me know how you get on. It wouldn’t surprise me if at least one
of the package makefiles, hol.mkf, zed.mkf etc. does something that
depends on pptex or TeX or LaTeX, but that should be fixable.

Note xpp needs groff to build, but you could you could uninstall it
afterwards. However, groff is tiny compared with TeX and LaTeX.

If we can get it to work, I can make it something that you can select
via an environment variable when you run configure.

Regards,

Rob.

> On 5 Jun 2015, at 23:26, Daniel Moniz <d...@pobox.com> wrote:
> 
> Hi Rob,
> 
> I'm having an issue building OpenProofPower-3.1w5 on Xubuntu (Ubuntu)
> 14.04 LTS (64-bit). Here are the last few lines of my build.log:
> 
> [ -d   "/home/dnm/pp"/doc ] || mkdir "/home/dnm/pp"/doc
> doctex  dtd017.doc
> texdvi -b dtd017 > dtd017.dvi.ldd1 </dev/null
> make: *** [dtd017.dvi] Error 1
> rm dtd017.tex
> 
> This seems to happen regardless of trying some tweaks, like setting
> PPTARGETS to not include pptex (e.g. PPTARGETS="dev xpp hol zed daz"),
> and/or running install post-./configure as just "./install +d"; I admit
> that I'm kind of thrashing around and trying things based on the
> instructions at http://www.lemma-one.com/ProofPower/getting/README that
> don't expressly say they will help solve this issue.
> 
> Ideally the tools would build without needing to generate DVI
> information at all if specifically requested not to, but that's just me.
> I guess *ideally* there wouldn't be an issue with the TeX/DVI side of
> things so wanting to not need any of the DVI files wouldn't be required.
> But it does seem that OpenProofPower really can't be built at all
> without TeX/LaTeX/DVI in the mix somewhere, which, in fairness, Section
> 2 of the README does say:
> 
> "[...] You certainly need:"
> ...
> "e) the Tex and LaTeX typesetting software"
> 
> I'm just trying to build and run in a modestly sized VM, and thus trying
> to get away with the smallest TeX install I can since a full install
> chews up all my disk space and more. I was hoping I could build and use
> OpenProofPower without any TeX/LaTeX tools *required*, and have it spit
> out LaTeX sources, etc. that I could move/copy to typeset on my Windows
> or OS X machine (where I have plenty of disk space, and full TeX Live
> installs). As it is, I surrendered to installing "texlive-latex-base"
> from the Ubuntu repository (plus its dependencies), but I'm still
> getting the error above. It's also not very informative, so I'm not sure
> what is breaking such that make-ing that dvi file fails. texdvi is built
> and seems to be fine (displays usage).
> 
> Any hints?
> 
> Thanks in advance, thanks for making OpenProofPower, and for making it
> available.
> 
> 
> -- 
> Daniel Moniz <d...@pobox.com> [http://pobox.com/~dnm/]
> 


_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to