Maude-help mailing list

[Paco Durán <fdm AT uma.es>]

Hi Michael,

It would have saved you some time... The link to the available information on 
compiling in Cygwin is in the first sentence of the page on installation 
(http://maude.cs.illinois.edu/w/index.php?title=Maude_download_and_installation).
 Nevertheless, if you think there is some missing info or want to suggest 
something to improve its current state, please, go ahead, I'll do my best to 
implement it. 

Regarding documentation on the use of CVC4 from Maude, I'm afraid the answer 
is no. All we currently have are the beta release notes and some experiments. 
We won't prepare the documentation until it is fully integrated and we decide 
to include it in an official release. 

Cheers,

Francisco

> On 24 Dec 2016, at 19:29, Michael George Hart 
> <michael.george.hart AT gmail.com>
>  wrote:
> 
> Thanks for the Information
> 
> It would have been nice to conveniently find this on the Wiki for the Maude 
> System website rather than reinventing the wheel
> 
> Are there any tutorials/documentation about using CVC4 from the Maude 
> System?
> 
> Michael Hart
> 
> 
> 
> On Friday, December 23, 2016, Julia Sapiña Sanchis 
> <jsapina AT dsic.upv.es>
>  wrote:
> Dear Michael,
> 
> 
> Just in case you need it, there is a detailed, updated (to Maude 2.7.1) 
> guide to compile Maude on Windows available at
> 
> http://safe-tools.dsic.upv.es/maude
> 
> which is based on the (now outdated) original guide written by José María 
> Álvarez Palomo available at
> 
> http://maude.cs.uiuc.edu/download/windows.html
> 
> 
> Actually, the first release of the guide was announced here last year:
> 
> https://lists.cs.illinois.edu/lists/arc/maude-help/2015-09/msg00001.html
> 
> 
> Best regards,
> 
> Julia
> 
> 
> El 23/12/2016 a las 20:04, Michael George Hart escribió:
> This is a guide that primary to shows you how to build Maude system for
> the MS Windows, what is learned here can be applied to the UNIX/LINUX
> environment
> 
> If you are able to improve upon what I have done; please do so and add
> it to the Maude documentation
> 
> cygwin 2.5.1 what I used as my build environment under MS Windows. Doing
> the command "uname"
> 
> $ uname -srvm
> CYGWIN_NT-6.1 2.5.1(0.297/5/3) 2016-04-21 22:14 x86_64
> 
> 
> ./configure  --build=x86_64-pc-cygwin --host=x86_64-pc-cygwin
> --target=x86_64-pc-cygwin CFLAGS="-O2 -D_POSIX_C_SOURCE=1"
> Manual setting of --build, --host and --target configuration parameters
> were required because the configuration scripts were having problems
> discovering the respective parameters.  A quick and dirty way to
> discover those parameters is run "gcc -v" at the command line and copy
> the desire parameters displayed.
> 
> On my installation of cygwin gcc -v showed "--build=x86_64-pc-cygwin
> --host=x86_64-pc-cygwin --target=x86_64-pc-cygwin" so for all libraries
> and maude I appended "--build=x86_64-pc-cygwin --host=x86_64-pc-cygwin
> --target=x86_64-pc-cygwin" to configuration
> 
> NOTE: I use the make option "-j" to improve build time in all cases.
> 
> _*Building BuDDy*_
> https://sourceforge.net/projects/buddy/
> <https://urldefense.proofpoint.com/v2/url?u=https-3A__sourceforge.net_projects_buddy_&d=DQMFaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=2MKLCGaRz6F7d1qtLDSBJpRohhXrqUfSda0wBU0VRHo&m=vtKibOu2KdOKr4-8BnJdlGLwCGksbxKlotdEgt_TigU&s=kScuTKRQikAvtcHle08uCaU_oNxY9FmjdhgZiuFviwA&e=>
> tar -xvzf <buddy tar gz file>
> cd <BuDDy extract directory>
> ./configure  --build=x86_64-pc-cygwin --host=x86_64-pc-cygwin
> --target=x86_64-pc-cygwin
> make -j12
> make install
> 
> _*Building Tecla*_
> http://www.astro.caltech.edu/~mcs/tecla/index.html
> <https://urldefense.proofpoint.com/v2/url?u=http-3A__www.astro.caltech.edu_-257Emcs_tecla_index.html&d=DQMFaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=2MKLCGaRz6F7d1qtLDSBJpRohhXrqUfSda0wBU0VRHo&m=vtKibOu2KdOKr4-8BnJdlGLwCGksbxKlotdEgt_TigU&s=3-Z8aJkOPng1JxwuYsURCtjVEJvtzVlnvZr7ObQ8Pck&e=>
> tar -xvzf <libtecla tar gz file>
> cd <libTecla extract directory>
> ./configure  --build=x86_64-pc-cygwin --host=x86_64-pc-cygwin
> --target=x86_64-pc-cygwin CFLAGS="-O2 -D_POSIX_C_SOURCE=1"
> cat \
> make TARGETS=normal TARGET_LIBS=static install
> 
> _*Building CVC4*_
> This is an optional module for the Maude System. I would not recommend
> you building it unless you truly desire its features in the Maude
> System; it takes forever to build and cause extensive start up time for
> the Maude System... see the Maude INSTALL/README
> 
> http://cvc4.cs.nyu.edu/web/
> <https://urldefense.proofpoint.com/v2/url?u=http-3A__cvc4.cs.nyu.edu_web_&d=DQMFaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=2MKLCGaRz6F7d1qtLDSBJpRohhXrqUfSda0wBU0VRHo&m=vtKibOu2KdOKr4-8BnJdlGLwCGksbxKlotdEgt_TigU&s=buLYxKbZSoQShM81k8pnTH5J8YsY7LLOXuKtqtDkQOM&e=>
> To build CVC4, you will first need to install and build the *ANTLR3 C
> runtime* *libantlr3c-3.4.tar.gz* which can be found here
> http://www.antlr3.org/download.html
> <https://urldefense.proofpoint.com/v2/url?u=http-3A__www.antlr3.org_download.html&d=DQMFaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=2MKLCGaRz6F7d1qtLDSBJpRohhXrqUfSda0wBU0VRHo&m=vtKibOu2KdOKr4-8BnJdlGLwCGksbxKlotdEgt_TigU&s=GXGN3-qc598p9OmhpICqnz6--W4FMD_TMb_o8sEfxi4&e=>
> and then navigate to here  http://www.antlr3.org/download/C/
> <https://urldefense.proofpoint.com/v2/url?u=http-3A__www.antlr3.org_download_C_&d=DQMFaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=2MKLCGaRz6F7d1qtLDSBJpRohhXrqUfSda0wBU0VRHo&m=vtKibOu2KdOKr4-8BnJdlGLwCGksbxKlotdEgt_TigU&s=Imp2sWJWGa52FwLu28qXnPVRomuHFOgOQXkS0REg6Yk&e=>
> Performing the following commands will get the ANTLR3 C runtime
> installed into your _*cygwin system*_:
> tar -xvzf libantlr3c-3.4.tar.gz
> cd <libantlr3 extract directory>
> ./configure  --build=x86_64-pc-cygwin --host=x86_64-pc-cygwin
> --target=x86_64-pc-cygwin
> make -j12
> make install
> 
> _/*Now you are ready to build cvc4*/_
> tar -xvzf cvc4-2016-12-15.tar.gz
> cd <cvc4 extract directory>
> ./configure  --build=x86_64-pc-cygwin --host=x86_64-pc-cygwin
> --target=x86_64-pc-cygwin --enable-language-bindings=c,c++
> make -j12
> make install
> 
> _*Building Maude*_
> tar -xvzf Maude-2.7.1.tar.gz
> cd <maude extract directory>
> mkdir build
> cd build
> 
> if you want maude /_*without cvc4*_/ do the following:
> ../configure  --build=x86_64-pc-cygwin --host=x86_64-pc-cygwin
> --target=x86_64-pc-cygwin --with-cvc4=no
> BUDDY_LIB=/usr/local/lib/libbdd.a TECLA_LIBS="/usr/local/lib/libtecla.a
> -lcurses"
> 
> with cvc4
> ../configure  --build=x86_64-pc-cygwin --host=x86_64-pc-cygwin
> --target=x86_64-pc-cygwin CVC4_LIB=/usr/local/lib/libcvc4.a
> BUDDY_LIB=/usr/local/lib/libbdd.a TECLA_LIBS="/usr/local/lib/libtecla.a
> -lcurses"
> 
> make -j12
> 
> *NOTE:* */On my system I eventually get an error (see the message I get
> above) when the error I start make without the "-j12" ... there seems to
> be a problem with the multi threading when the make file is being
> executed for bison.... just enter make again at the command line to
> continue the process
> /*
> 
> make
> make install
> 
> NOTE: The error I eventually get when using /*make -j12*/ building the
> maude sytem
> /../../../src/Mixfix/top.yy \/
> //
> /../../../src/Mixfix/modules.yy \/
> //
> /../../../src/Mixfix/commands.//yy \/
> //
> /../../../src/Mixfix/bottom.yy \/
> //
> /> surface.yy/
> //
> /bison -dv surface.yy -o surface.c/
> //
> /bison -dv surface.yy -o surface.c/
> //
> /mv surface.c surface.cc/
> //
> /mv surface.c surface.cc/
> //
> /flex -t -p -p ../../../src/Mixfix/lexer.ll > lexer.cc/
> //
> /mv: cannot stat 'surface.c': No such file or directory/
> //
> /Makefile:1324: recipe for target 'surface.cc' failed/
> //
> /make[3]: *** [surface.cc] Error 1/
> //
> 
> 
> ll that is left to do is tell the Maude System where the prelude.maude
> and associated files are found.
> export MAUDE_LIB=/usr/local/share
> 
> Good luck
> 
> Could some one please add these instruction to the Maude System Wiki
> 
> Thanks
> Michael
> --
> /*"...Hope is what makes us strong. It is why we are here. It is what we
> fight with when all is lost..."*/
> 
> 
> -- 
> "...Hope is what makes us strong. It is why we are here. It is what we 
> fight with when all is lost..."