Closed HenriqueMisson closed 5 years ago
anmaped
commented
5 years ago You are using /home/labvant/ardupilot/modules/PX4NuttX/nuttx/include/stdio.h and /opt/gcc-arm-none-eabi-4_9-2015q3/arm-none-eabi/include/wchar.h at the same time and both define the symbol FILE.
BTW, you have to setup the nuttx environment variables correctly.
anmaped
commented
5 years ago Could you test the rmtld3synth version 0eb492f8d6eec6ac67cb6c41cae7cf9058be6f85? The makefile is now fixed.
HenriqueMisson
commented
5 years ago I update my repository and nothing was changed.
To see these changes I need to recompiled and reinstall the toolchain?
anmaped
commented
5 years ago Just reinstall rmtld3synth using opam and re-pin the package if needed.
opam remove rmtld3synth
opam pin add rmtld3synth https://github.com/anmaped/rmtld3synth.git
# or just
opam install rmtld3synthI used to remove rmtld3synth and reinstall with opam pin add. But now, I'm in the same issue as #1 : # ocamlfind: package 'z3' not found
As you suggested , I typed ocamlfind query Z3/z3 and it was found just Z3 ( /home/labvant/.opam/4.03.0/lib/Z3). In this sense, I have already searched that ocamlfind is a case sensitive, but I didn't find where to change the name.
In the topic that I saw, the person changed the "_tags file contained true: package(Z3), I just changed it to true: package(z3)"
Do you know where I should to change?
anmaped
commented
5 years ago Just re-install.
HenriqueMisson
commented
5 years ago I tried both opam pin add rmtld3synth https://github.com/anmaped/rmtld3synth.git and opam install rmtld3synth and now I have other error: Error: This expression has type Dolmen.Term.t but an expression was expected of type string * Dolmen.Statement.term option
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[ERROR] The compilation of rmtld3synth failed at "make all".
Processing 1/1: [rmtld3synth: ocamlfind remove]
#=== ERROR while installing rmtld3synth.0.3-dev ===============================#
# opam-version 1.2.2
# os linux
# command make all
# path /home/labvant/.opam/4.03.0/build/rmtld3synth.0.3-dev
# compiler 4.03.0
# exit-code 2
# env-file /home/labvant/.opam/4.03.0/build/rmtld3synth.0.3-dev/rmtld3synth-7508-a71bb4.env
# stdout-file /home/labvant/.opam/4.03.0/build/rmtld3synth.0.3-dev/rmtld3synth-7508-a71bb4.out
# stderr-file /home/labvant/.opam/4.03.0/build/rmtld3synth.0.3-dev/rmtld3synth-7508-a71bb4.err
### stdout ###
# [...]
# findlib: [WARNING] Interface myocamlbuild.cmi occurs in several directories: ., /home/labvant/.opam/4.03.0/lib/dolmen
# ocamlfind ocamlc -c -warn-error A -package unix,type_conv,sexplib,batteries,Z3,dolmen -package dolmen -I src -I src/language -o src/language/smtlib2.cmo src/language/smtlib2.ml
# + ocamlfind ocamlc -c -warn-error A -package unix,type_conv,sexplib,batteries,Z3,dolmen -package dolmen -I src -I src/language -o src/language/smtlib2.cmo src/language/smtlib2.ml
# findlib: [WARNING] Interface myocamlbuild.cmi occurs in several directories: ., /home/labvant/.opam/4.03.0/lib/dolmen
# File "src/language/smtlib2.ml", line 33, characters 30-205:
# Error: This expression has type Dolmen.Term.t
# but an expression was expected of type
# string * Dolmen.Statement.term option
# Command exited with code 2.
# Makefile:12: recipe for target 'all' failed
### stderr ###
# make: *** [all] Error 10
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
∗ install rmtld3synth 0.3-dev
No changes have been performed
[NOTE] Pinning command successful, but your installed packages may be out of sync.Just do opam pin add dolmen https://github.com/Gbury/dolmen.git. Check https://github.com/anmaped/rmtld3synth/blob/master/.travis-opam.sh for reference since you are using a dev version.
The issue is that we are using dev versions of other packages and no release is done yet. Then, we have to compile them from the last git version.
I will add that dependency check to the configure phase to avoid further issues.
HenriqueMisson
commented
5 years ago I rebuild all from zero and now I tried opam pin add dolmen https://github.com/Gbury/dolmen.git, but I still have problems. From now is to install dolmen dev as you commented.
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[ERROR] The compilation of dolmen failed at "dune subst".
#=== ERROR while installing dolmen.dev ========================================#
# opam-version 1.2.2
# os linux
# command dune subst
# path /home/labvant/.opam/4.03.0/build/dolmen.dev
# compiler 4.03.0
# exit-code 1
# env-file /home/labvant/.opam/4.03.0/build/dolmen.dev/dolmen-3944-d8a4ae.env
# stdout-file /home/labvant/.opam/4.03.0/build/dolmen.dev/dolmen-3944-d8a4ae.out
# stderr-file /home/labvant/.opam/4.03.0/build/dolmen.dev/dolmen-3944-d8a4ae.err
### stderr ###
# [...]
# | Called from file "src/fiber/fiber.ml", line 56, characters 6-20
# |
# | Original exception was: Stdune__Exn.Code_error(_)
# | Called from file "camlinternalLazy.ml", line 27, characters 17-27
# | Re-raised at file "camlinternalLazy.ml", line 34, characters 10-11
# | Called from file "src/errors.ml", line 77, characters 17-47
# | Called from file "format.ml", line 1247, characters 20-38
# | Called from file "src/stdune/option.ml", line 23, characters 14-17
# | Called from file "src/fiber/fiber.ml", line 243, characters 6-18
# \-----------------------------------------------------------------------
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
∗ install dolmen dev
No changes have been performed
[NOTE] Pinning command successful, but your installed packages may be out of sync.Why opam install directly the branch dev from dolmen. It don't have just a dolmen?
anmaped
commented
5 years ago @HenriqueMisson Could you try to install dune by typing opam install dune ?
HenriqueMisson
commented
5 years ago I installed dune, Package dune is already installed (current version is 1.2.1)., but I can't install dolmen.
anmaped
commented
5 years ago Could you give me the full log ?
HenriqueMisson
commented
5 years ago labvant@labvant:~$ opam pin add dolmen https://github.com/Gbury/dolmen.git
[NOTE] Package dolmen is already git-pinned to
https://github.com/Gbury/dolmen.git.
This will erase any previous custom definition.
Proceed ? [Y/n] y
[dolmen] https://github.com/Gbury/dolmen.git updated
[dolmen] Installing new package description from
https://github.com/Gbury/dolmen.git
dolmen needs to be installed.
The following actions will be performed:
∗ install dolmen dev*
Do you want to continue ? [Y/n] y
=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[dolmen] https://github.com/Gbury/dolmen.git already up-to-date
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[ERROR] The compilation of dolmen failed at "dune subst".
#=== ERROR while installing dolmen.dev ========================================#
# opam-version 1.2.2
# os linux
# command dune subst
# path /home/labvant/.opam/4.03.0/build/dolmen.dev
# compiler 4.03.0
# exit-code 1
# env-file /home/labvant/.opam/4.03.0/build/dolmen.dev/dolmen-31702-d8a4ae.env
# stdout-file /home/labvant/.opam/4.03.0/build/dolmen.dev/dolmen-31702-d8a4ae.out
# stderr-file /home/labvant/.opam/4.03.0/build/dolmen.dev/dolmen-31702-d8a4ae.err
### stderr ###
# [...]
# | Called from file "src/fiber/fiber.ml", line 56, characters 6-20
# |
# | Original exception was: Stdune__Exn.Code_error(_)
# | Called from file "camlinternalLazy.ml", line 27, characters 17-27
# | Re-raised at file "camlinternalLazy.ml", line 34, characters 10-11
# | Called from file "src/errors.ml", line 77, characters 17-47
# | Called from file "format.ml", line 1247, characters 20-38
# | Called from file "src/stdune/option.ml", line 23, characters 14-17
# | Called from file "src/fiber/fiber.ml", line 243, characters 6-18
# \-----------------------------------------------------------------------
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
∗ install dolmen dev
No changes have been performed
[NOTE] Pinning command successful, but your installed packages may be out of sync.I mean the files /home/labvant/.opam/4.03.0/build/dolmen.dev/dolmen-31702-d8a4ae.out and /home/labvant/.opam/4.03.0/build/dolmen.dev/dolmen-31702-d8a4ae.err
HenriqueMisson
commented
5 years ago I'm sorry. The file ".out" is empty and the file ".err" has:
/-----------------------------------------------------------------------
| Internal error: Fiber.Execution_context.forward_error: error handler raised.
| Stdune__Exn.Code_error(_)
| Called from file "camlinternalLazy.ml", line 27, characters 17-27
| Re-raised at file "camlinternalLazy.ml", line 34, characters 10-11
| Called from file "src/errors.ml", line 77, characters 17-47
| Called from file "format.ml", line 1247, characters 20-38
| Called from file "src/stdune/option.ml", line 23, characters 14-17
| Called from file "src/fiber/fiber.ml", line 243, characters 6-18
| Called from file "src/fiber/fiber.ml", line 56, characters 6-20
|
| Original exception was: Stdune__Exn.Code_error(_)
| Called from file "camlinternalLazy.ml", line 27, characters 17-27
| Re-raised at file "camlinternalLazy.ml", line 34, characters 10-11
| Called from file "src/errors.ml", line 77, characters 17-47
| Called from file "format.ml", line 1247, characters 20-38
| Called from file "src/stdune/option.ml", line 23, characters 14-17
| Called from file "src/fiber/fiber.ml", line 243, characters 6-18
\-----------------------------------------------------------------------Try opam update and then try to re-install a new version of dune.
HenriqueMisson
commented
5 years ago I updated my opam, and I tried to install the new version of dune (1.5.1) with the command opam install dune, as pin the new repository, but I always come to the same version "dune.1.2.1".
Do you think a good way download the source from the site " https://opam.ocaml.org/packages/dune/" ?
anmaped
commented
5 years ago Try to checkout the repo in https://github.com/ocaml/dune and do
$ make release
$ make installI'm using that version right now. You shouldn't forget to uninstall old dune first.
HenriqueMisson
commented
5 years ago I don't know what is happen.
I uninstall dune (opam remove dune), after I cloned the repo "dune" that you gave me. I compiled and installed dune as you said (make release and sudo make install). So I got
./_build/default/bin/main_dune.exe install dune
opam (internal)
[WARNING] Running as root is not recommended
Done: 0/0 (jobs: 1)Installing /usr/local/lib/ocaml/4.02.3/dune/META
Installing /usr/local/lib/ocaml/4.02.3/dune/_caml/dune._caml.dune
...
Installing /home/labvant/.opam/4.03.0/man/man5/dune-config.5and installing all that is described in "dune.install".
After that I tried some things:
opam pin add dolmen https://github.com/Gbury/dolmen.git : but it needs to install "dune 1.2.1* " and we get the same error.
Clone the dolmen repo from git and install manually (make -C src and make -C src install) and to compile I had a message that it don't have "makefile". So I tried only make and I got the message :
dune build --profile release
make: dune: Command not found
Makefile:10: recipe for target 'dune' failed
make: *** [dune] Error 127Pin "dune" to opam, but it always install "dune 1.2.1"
So I couldn't install correctly "rmtld3synth" that needs "dolmen" that need "dune".
Do you have any idea?
PS: I'm sorry for that work, but considering that your toolchain is the only I know that can be implemented in my context, I really need it.
anmaped
commented
5 years ago @HenriqueMisson You can check at https://opam.ocaml.org/packages/dune/ that the last version of dune is 1.5.1. Try to update opam.
anmaped
commented
5 years ago I think I found a clue for you, so unpin dune first (opam unpin dune) and then install dune using opam pin add dune https://github.com/ocaml/dune/releases/download/1.5.0/dune-1.5.0.tbz.
HenriqueMisson
commented
5 years ago I think I could install. In opam list I have: rmtld3synth 0.3-dev (pinned)
And when I type which rmtld3synth I have as output /home/labvant/.opam/4.03.0/bin/rmtld3synth
But I don't have the folder "rmtld3synth". Should I clone it from github and after install with make and sudo make install commands?
anmaped
commented
5 years ago You have the binary installed in /home/labvant/.opam/4.03.0/bin/rmtld3synth. Why you need the folder and why you need to do make?
BTW, you can check the version you are using with rmtld3synth --version.
HenriqueMisson
commented
5 years ago You have the binary installed in
/home/labvant/.opam/4.03.0/bin/rmtld3synth. Why you need the folder and why you need to do make?
I'm sorry for the question, but I've never used opam before. The "bin" folder from opam is in my PATH, but I tried to synthesize the monitor as demonstrated by you in the readme,and I have an error like Fatal error: exception (Sys_error "config/default: No such file or directory")
BTW, you can check the version you are using with
rmtld3synth --version.
Ok. My version in the case is Git version v0.3-alpha2-16-gc8f7357 (c8f735745b744fa26f345ca77bcc8b3d7bc60c55)
anmaped
commented
5 years ago So everything is right. You are with the last version.
Regarding the config/default, you have to use the flag --config-file and use the proper config file.
Edit: you can check some configuration example in https://github.com/anmaped/rmtld3synth/tree/master/config
HenriqueMisson
commented
5 years ago Ok, thank you very much for your help André.
Just one other question. I tried to install in other machine, and I got the error
[ERROR] The compilation of rmtld3synth failed at "make all".
#=== ERROR while installing rmtld3synth.0.3-dev ===============================#
# opam-version 1.2.2
# os linux
# command make all
# path /home/henrique/.opam/4.03.0/build/rmtld3synth.0.3-dev
# compiler 4.03.0
# exit-code 2
# env-file /home/henrique/.opam/4.03.0/build/rmtld3synth.0.3-dev/rmtld3synth-3121-a71bb4.env
# stdout-file /home/henrique/.opam/4.03.0/build/rmtld3synth.0.3-dev/rmtld3synth-3121-a71bb4.out
# stderr-file /home/henrique/.opam/4.03.0/build/rmtld3synth.0.3-dev/rmtld3synth-3121-a71bb4.err
### stdout ###
# echo "let git = \"`git describe --tags` (`git rev-parse HEAD`)\n`uname -m -o` `date +\"%Y-%m-%d %H:%M\"`\"" > src/version.ml
# cp src/interface/z3solver_newAPI.ml src/interface/z3solver_.ml
# cp src/interface/mathkernel_call.ml src/interface/mathkernel_call_.ml
# echo "(* dummy js interface *)" >> src/js/helper_.ml
# dune build --profile release @install
# Makefile:12: recipe for target 'all' failed
### stderr ###
# File "src/interface/dune", line 5, characters 89-91:
# 5 | (libraries rmtld3synth.helper rmtld3synth.rmtld3.extension sexplib ppx_sexp_conv Z3)
# ^^
# Error: Library "Z3" not found.
# Hint: try: dune external-lib-deps --missing --profile release @install
# make: *** [all] Error 1
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
∗ install rmtld3synth 0.3-dev
No changes have been performedI think is due to the ocamlfind that is case sensitive, because I have z3 and not Z3
henrique@henrique-VirtualBox:~$ ocamlfind query z3
/home/henrique/.opam/4.03.0/lib/z3
henrique@henrique-VirtualBox:~$ ocamlfind query Z3
ocamlfind: Package `Z3' not foundDo you know what I can do to solve this?
anmaped
commented
5 years ago How have you installed z3 and which version?
HenriqueMisson
commented
5 years ago By typing opam install z3 and the version installed was Z3 version 4.8.4 - 64 bit
anmaped
commented
5 years ago ok. Just replace Z3 to z3 in src/interface/dune.
anmaped
commented
5 years ago Could you verify if the same happens with Z3 4.7.x ?
HenriqueMisson
commented
5 years ago ok. Just replace Z3 to z3 in
src/interface/dune.
I had already done that, but I have re-installed rmtld3synth and the file was replaced. So, I did this again and then make all. From now I have the error:
File "src/interface/z3solver_.ml", line 21, chaaracters 5-23:
Error: Unbound module Rmtld3synth_helperDo I need to change all "Z3" to "z3" in this file too?
anmaped
commented
5 years ago First, test Z3 4.7.x or compile Z3 manually. I have to know why Z3 changed to z3 and if it is a matter of the opam package or the z3 git version Makefile.
HenriqueMisson
commented
5 years ago I tried to install Z3 4.7.1 by downloading the source code from https://github.com/z3prover/z3/releases and then the steps to compile it and install. I had the message Z3 was successfully installed., but when I tried to see the version, I had the message that "z3 is currently not installed".
So I tried to compile and install Z3 manually.
Now when I tried to install rmtld3synth I had other error in the compilation:
[ERROR] The compilation of rmtld3synth failed at "make all".
#=== ERROR while installing rmtld3synth.0.3-dev ===============================#
# opam-version 1.2.2
# os linux
# command make all
# path /home/henrique/.opam/4.03.0/build/rmtld3synth.0.3-dev
# compiler 4.03.0
# exit-code 2
# env-file /home/henrique/.opam/4.03.0/build/rmtld3synth.0.3-dev/rmtld3synth-7460-ad8886.env
# stdout-file /home/henrique/.opam/4.03.0/build/rmtld3synth.0.3-dev/rmtld3synth-7460-ad8886.out
# stderr-file /home/henrique/.opam/4.03.0/build/rmtld3synth.0.3-dev/rmtld3synth-7460-ad8886.err
### stdout ###
# echo "let git = \"`git describe --tags` (`git rev-parse HEAD`)\n`uname -m -o` `date +\"%Y-%m-%d %H:%M\"`\"" > src/version.ml
# cp src/interface/z3solver.ml src/interface/z3solver_.ml
# cp src/interface/mathkernel_call.ml src/interface/mathkernel_call_.ml
# echo "(* dummy js interface *)" >> src/js/helper_.ml
# dune build --profile release @install
# Makefile:12: recipe for target 'all' failed
### stderr ###
# File "dune-project", line 1, characters 11-14:
# 1 | (lang dune 1.5)
# ^^^
# Error: Version 1.5 of dune is not supported.
# Supported versions:
# - 0.0
# - 1.0 to 1.2
# make: *** [all] Error 1
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
∗ install rmtld3synth 0.3-dev
No changes have been performedHowever, if I see the dune version I have: "1.2.1".
anmaped
commented
5 years ago So it says Error: Version 1.5 of dune is not supported.. Why have you not installed dune 1.5 ? You need dune 1.5.
anmaped
commented
5 years ago The z3 package spelling issue is now managed automatically in 0273fcaa5484f6689c36ae9190e406ab9b87649b.
HenriqueMisson
commented
5 years ago So it says
Error: Version 1.5 of dune is not supported.. Why have you not installed dune 1.5 ? You need dune 1.5.
Dune was automatically installed. I though that the versions 1.5 was not supported by rmtld3synth
HenriqueMisson
commented
5 years ago Now I got it.
Thank you again André.
anmaped
commented
5 years ago rmtld3synth is now using dune since commit e75d324f40f0fbfdf1e60ba51b876430d4cbc12c.
HenriqueMisson
commented
5 years ago Andre, to write monitors in this new version we need to include the flag --config/file as you said. But this file can be for exemple the default (config/default)? What do you call "file" in this context? I tried many combinations, but I could not generate a monitor.
I mean, if we want to generate the exemple monitor rmtld3synth --synth-cpp11 --input-latexeq "(a \rightarrow ((a \lor b) \until_{<10} c)) \land \int^{10} c < 4" --out-src="mon1" we need to add the flag --config/file?
anmaped
commented
5 years ago Yes. It's right.
An example could be
(buffer_size 100)
(maximum_inter_arrival_time 1)
(maximum_period 2000000)
(event_type Event)
(event_subtype int)
(cluster_name mon1)Check section doc/general.md#overview-of-the-configuration-file.
Hello Andre,
I generated a monitor with the command
./rmtld3synth --synth-cpp11 --input-latexeq "(a \rightarrow ((a \lor b) \until_{<10} c)) \land \int^{10} c < 4" --out-src="mon1"as demonstrated in the readme.I modified the Makefile to take the correct files path as:
I'm using the toolchain arm-none-eabi version 4.9.3. And when I compile with
make arm-monI have these errors:Could you help me in this sense, please? I tried many things to fix the errors, but I couldn't resolve.