Maude-help mailing list

[Michael George Hart <michael.george.hart AT gmail.com>]

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..."