[Caml-list] ocamlbuild - which source files for tag declarations?
Hi,
I'm having difficulties understanding on which files I should declare
tags: *.ml, or *.cmo/cmx?
For instance, with normal (non-parameterized) tags, declaring the tag
on the .cmo/.cmx seems to have no effect on the compilation, for
instance:
$ cat _tags
<*.cmo>: annot
<*.cmx>: annot
$ ocamlbuild -classic-display A.cmo A.cmx
/usr/pkg/bin/ocamldep.opt -modules A.ml > A.ml.depends
/usr/pkg/bin/ocamlc.opt -c -o A.cmo A.ml
/usr/pkg/bin/ocamlopt.opt -c -o A.cmx A.ml
Here, tagging *.cmo/cmx has no effect. The _build/_log says:
# Target: A.cmo, tags: { byte, compile, extension:ml, file:A.ml, implem,
ocaml, quiet, traverse }
The tag annot is not there. But if *.ml is used instead of *.cmo in
_tags, then the tag appears in the above target. Does this mean that
tags to customize compilation commands should be declared on the *.ml
files? (Hence they necessarily apply to both .cmo and .cmx files?)
The situation looks a bit different with parameterized tags, for
instance :
$ cat _tags
<*.cmo>: pp(foo)
<*.cmx>: pp(foo)
$ ocamlbuild -classic-display A.cmo A.cmx
/usr/pkg/bin/ocamldep.opt -modules A.ml > A.ml.depends
/usr/pkg/bin/ocamlc.opt -c -o A.cmo A.ml
/usr/pkg/bin/ocamlopt.opt -c -pp foo -o A.cmx A.ml
Here, the pp(foo) tag is ignored for the *.cmo declaration, but it is
used for the *.cmx declaration. Is this behavior intended? The code
says (ocaml_specific.ml):
pflag ["ocaml"; "compile"] "pp"
(fun param -> S [A "-pp"; A param]);
So I wonder why pp(foo) only applies to *.cmx.
Thanks for your help,
Grégoire
___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] Job offer at LexiFi
Job offer: use the approaches, languages, and tools that you like... every day!
LexiFi is a financial software vendor based in Paris (Boulogne-Billancourt).
The strong theoretical computer science culture that pervades our firm has
enabled us to develop approaches and tools that radically simplify the
development of financial applications. LexiFis offering is based on an
original formalism for describing financial contracts.
LexiFi is seeking talented and formally-trained (Master or PhD level) computer
scientists to enlarge its R&D team.
You will be exposed to many aspects of our technology. We use functional
programming languages for both our core functionality (financial domain) and
other developments (user interface, database interface, interface with other
software, etc.).
Since we develop most of our software with an extension of OCaml, good
functional programming skills are required. A taste for mathematics is a plus.
An interest in software quality issues is desirable.
If you want to join a motivating yet friendly environment that fosters quality,
in which you can apply your skills, work with tools that you like, learn
original software and financial engineering techniques, and assume growing
responsibilities, please send a letter and a resume to care...@lexifi.com.
For more information, visit http://www.lexifi.com.
---
Offre demploi : utilisez tous les jours les approches, langages et outils que
vous aimez !
LexiFi est un éditeur de logiciels financiers situé à Paris
(Boulogne-Billancourt).
Forts d'une culture en informatique théorique, nous développons des approches
et des outils qui simplifient radicalement le développement dapplications
financières. Loffre de LexiFi repose sur un formalisme original et rigoureux
de description des contrats financiers.
LexiFi cherche des informaticiens de haut niveau pour renforcer son équipe de
R&D.
Vous serez amené(e) à intervenir sur de multiples facettes de notre
technologie. Nous utilisons les langages fonctionnels tant dans notre cur de
produit ("finance") que dans tous les autres développements (interface
utilisateur, interface bases de données, interface avec dautres logiciels
etc.).
Nos développements étant principalement réalisés en une extension de OCaml, une
bonne expérience en programmation fonctionnelle est nécessaire. Un goût pour
les mathématiques est un plus. Une sensibilité forte à la qualité logicielle
est souhaitable.
Si vous souhaitez rejoindre un environnement convivial favorisant la qualité,
lémulation et lentraide dans lequel vous pourrez appliquer vos connaissances,
utiliser les outils que vous aimez, apprendre des techniques informatiques et
financières originales et assumer des responsabilités croissantes, envoyez une
lettre de motivation et un CV à care...@lexifi.com.
Pour plus d'information, visitez http://www.lexifi.com.
___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] Postdoc positions available
[ Apologies for multiple copies of this message ] Post-Doc Positions Available Embedded System Research Unit Center for Information and Communication Technology Fondazione Bruno Kessler Trento, Italy !!! Application Deadline Approaching !!! The Embedded System Research Unit (http://es.fbk.eu) of the Information and Communication Technology Center of the Bruno Kessler Foundation, Trento, Italy, is seeking candidates for Post-Doc positions, to be hosted according to the call of proposal "Trentino - The Trentino programme of research, training and mobility of post-doctoral researchers", to be funded by the Autonomous Province of Trento, see: http://www.uniricerca.provincia.tn.it/binary/pat_uniricerca/news/call_1_post_doc_2010_incoming_en.1273589322.pdf Applications are invited in the broad field of formal verification and planning. Topics of interest include: - Model Checking - Safety Analysis - Schedulability - Planning and Run-time Monitoring Project proposals may have a duration of between two and three years. Candidate Profile = The ideal candidate should have a PhD degree in computer science, mathematics or electronic engineering, combine solid theoretical background and software development skills, and have some degree of autonomy. The candidate should be able to work in a collaborative environment, with a strong commitment to reaching research excellence and achieving assigned objectives. In depth previous experience in at least one of the following areas will be considered favorably: - Symbolic Model Checking - Propositional Satisfiability - Satisfiability Modulo Theory - Requirements Analysis - Constraint Solving and Optimization - Monitoring and Diagnosability - Software Verification - Safety Analysis (FTA, FMEA) We draw attention on the following requirements stated in the call for proposal. (1) The proposing researcher must have a PhD, obtained in Italy or abroad no more than three years before the deadline of this call. (2) The proposing researcher must not have had any working relationship (including any fellowship, scholarship, research grant, contract, cooperation) with any research organizations which have their registered office or operating centres inside Trento Province, longer than 30 days on the whole, during the two years before the deadline of this call. Applications and Inquiries == Potential candidates should express their interest and/or inquire for further information by sending email to . Applications should contain a statement of interest, with a Curriculum Vitae, and the names of three reference persons. PDF format is strongly encouraged. Emails will be automatically processed and should have 'RIF: ES/postdoc' as subject. Potential candidates will be interviewed in order to define the objectives of the research activities and to obtain the endorsement of the hosting institution. If successful, they will be required to complete the application through the PAT site by July 13th, 2010. The applications will be evaluated by an independent team of experts. The Embedded System Research Unit = The Embedded Systems Unit consists of about 15 persons, including researchers, post-Doc, PhD students, and programmers. The Unit carries out research, tool development and technology transfer in the fields of design and verification of embedded systems. Current research directions include: * Satisfiability Modulo Theory, and its application to the verification of hardware, embedded critical software, and hybrid systems (Verilog, SystemC, C/C++, StateFlow/Simulink) * Formal Requirements Analysis based on techniques for temporal logics (consistency checking, vacuity detection, input determinism, cause-effect analysis, realizability and synthesis) * Model-based engineering and formal verification of aerospace systems using model checking techniques, on-board reasoning systems for autonomous vehicles using planning techniques * Formal Safety Analysis, based on the integration of traditional techniques (e.g. Fault-tree analysis, FMEA) with symbolic verification techniques The unit develops and maintains several tools: * the NuSMV symbolic model checker (http://nusmv.fbk.eu) * the MathSAT SMT solver (http://mathsat.fbk.eu) * the Formal Safety Analysis Platform FSAP (http://fsap.fbk.eu) * the Requirements Analysis Tool RAT (http://rat.fbk.eu) The unit is currently involved in several research projects, funded by the European Union, the European Space Agency, the European Railway Agency, as well as in industrial technology transfer projects. The projects aim at applying research re
[Caml-list] Postdoc positions available
[ Apologies for multiple copies of this message ] Post-Doc Positions Available Embedded System Research Unit Center for Information and Communication Technology Fondazione Bruno Kessler Trento, Italy !!! Application Deadline Approaching !!! The Embedded System Research Unit (http://es.fbk.eu) of the Information and Communication Technology Center of the Bruno Kessler Foundation, Trento, Italy, is seeking candidates for Post-Doc positions, to be hosted according to the call of proposal "Trentino - The Trentino programme of research, training and mobility of post-doctoral researchers", to be funded by the Autonomous Province of Trento, see: http://www.uniricerca.provincia.tn.it/binary/pat_uniricerca/news/call_1_post_doc_2010_incoming_en.1273589322.pdf Applications are invited in the broad field of formal verification and planning. Topics of interest include: - Model Checking - Safety Analysis - Schedulability - Planning and Run-time Monitoring Project proposals may have a duration of between two and three years. Candidate Profile = The ideal candidate should have a PhD degree in computer science, mathematics or electronic engineering, combine solid theoretical background and software development skills, and have some degree of autonomy. The candidate should be able to work in a collaborative environment, with a strong commitment to reaching research excellence and achieving assigned objectives. In depth previous experience in at least one of the following areas will be considered favorably: - Symbolic Model Checking - Propositional Satisfiability - Satisfiability Modulo Theory - Requirements Analysis - Constraint Solving and Optimization - Monitoring and Diagnosability - Software Verification - Safety Analysis (FTA, FMEA) We draw attention on the following requirements stated in the call for proposal. (1) The proposing researcher must have a PhD, obtained in Italy or abroad no more than three years before the deadline of this call. (2) The proposing researcher must not have had any working relationship (including any fellowship, scholarship, research grant, contract, cooperation) with any research organizations which have their registered office or operating centres inside Trento Province, longer than 30 days on the whole, during the two years before the deadline of this call. Applications and Inquiries == Potential candidates should express their interest and/or inquire for further information by sending email to . Applications should contain a statement of interest, with a Curriculum Vitae, and the names of three reference persons. PDF format is strongly encouraged. Emails will be automatically processed and should have 'RIF: ES/postdoc' as subject. Potential candidates will be interviewed in order to define the objectives of the research activities and to obtain the endorsement of the hosting institution. If successful, they will be required to complete the application through the PAT site by July 13th, 2010. The applications will be evaluated by an independent team of experts. The Embedded System Research Unit = The Embedded Systems Unit consists of about 15 persons, including researchers, post-Doc, PhD students, and programmers. The Unit carries out research, tool development and technology transfer in the fields of design and verification of embedded systems. Current research directions include: * Satisfiability Modulo Theory, and its application to the verification of hardware, embedded critical software, and hybrid systems (Verilog, SystemC, C/C++, StateFlow/Simulink) * Formal Requirements Analysis based on techniques for temporal logics (consistency checking, vacuity detection, input determinism, cause-effect analysis, realizability and synthesis) * Model-based engineering and formal verification of aerospace systems using model checking techniques, on-board reasoning systems for autonomous vehicles using planning techniques * Formal Safety Analysis, based on the integration of traditional techniques (e.g. Fault-tree analysis, FMEA) with symbolic verification techniques The unit develops and maintains several tools: * the NuSMV symbolic model checker (http://nusmv.fbk.eu) * the MathSAT SMT solver (http://mathsat.fbk.eu) * the Formal Safety Analysis Platform FSAP (http://fsap.fbk.eu) * the Requirements Analysis Tool RAT (http://rat.fbk.eu) The unit is currently involved in several research projects, funded by the European Union, the European Space Agency, the European Railway Agency, as well as in industrial technology transfer projects. The projects aim at applying research re
