Byla vydána nová verze 5.4.0 programu na úpravu digitálních fotografií darktable (Wikipedie). Z novinek lze vypíchnout vylepšenou podporu Waylandu. Nejnovější darktable by měl na Waylandu fungovat stejně dobře jako na X11.
Byla vydána beta verze Linux Mintu 22.3 s kódovým jménem Zena. Podrobnosti v přehledu novinek a poznámkách k vydání. Vypíchnout lze, že nástroj Systémová hlášení (System Reports) získal mnoho nových funkcí a byl přejmenován na Informace o systému (System Information). Linux Mint 22.3 bude podporován do roku 2029.
GNU Project Debugger aneb GDB byl vydán ve verzi 17.1. Podrobný přehled novinek v souboru NEWS.
Josef Průša oznámil zveřejnění kompletních CAD souborů rámů tiskáren Prusa CORE One a CORE One L. Nejsou vydány pod obecnou veřejnou licenci GNU ani Creative Commons ale pod novou licencí OCL neboli Open Community License. Ta nepovoluje prodávat kompletní tiskárny či remixy založené na těchto zdrojích.
Nový CEO Mozilla Corporation Anthony Enzor-DeMeo tento týden prohlásil, že by se Firefox měl vyvinout v moderní AI prohlížeč. Po bouřlivých diskusích na redditu ujistil, že v nastavení Firefoxu bude existovat volba pro zakázání všech AI funkcí.
V pořadí šestou knihou autora Martina Malého, která vychází v Edici CZ.NIC, správce české národní domény, je titul Kity, bity, neurony. Kniha s podtitulem Moderní technologie pro hobby elektroniku přináší ucelený pohled na svět současných technologií a jejich praktické využití v domácích elektronických projektech. Tento knižní průvodce je ideální pro každého, kdo se chce podívat na současné trendy v oblasti hobby elektroniky, od
… více »Linux Foundation zveřejnila Výroční zprávu za rok 2025 (pdf). Příjmy Linux Foundation byly 311 miliónů dolarů. Výdaje 285 miliónů dolarů. Na podporu linuxového jádra (Linux Kernel Project) šlo 8,4 miliónu dolarů. Linux Foundation podporuje téměř 1 500 open source projektů.
Jean-Baptiste Mardelle se v příspěvku na blogu rozepsal o novinkám v nejnovější verzi 25.12.0 editoru videa Kdenlive (Wikipedie). Ke stažení také na Flathubu.
OpenZFS (Wikipedie), tj. implementace souborového systému ZFS pro Linux a FreeBSD, byl vydán ve verzi 2.4.0.
Kriminalisté z NCTEKK společně s českými i zahraničními kolegy objasnili mimořádně rozsáhlou trestnou činnost z oblasti kybernetické kriminality. V rámci operací OCTOPUS a CONNECT ukončili činnost čtyř call center na Ukrajině. V prvním případě se jednalo o podvodné investice, v případě druhém o podvodné telefonáty, při kterých se zločinci vydávali za policisty a pod legendou napadeného bankovního účtu okrádali své oběti o vysoké finanční částky.
17.2.2013 20:42
Bystroushaak | skóre: 36
| blog: Bystroushaakův blog
| Praha
Bez lidske inteligence si nemuze poradit ani s takovou trivialitou jako je treba odvozeni funkce (operatoru) nerovnosti:
AbcLinuxu.cz
ITBiz.cz
HDmag.cz
AbcPráce.cz-- nejprve operator ekvivalence
(==) :: Eq a => a -> a -> Bool
-- nerovnost ?
(/=) ? Eq a => a -> a -> Bool
-- error: cannot infer
-- musi natukat clovek
x /= y == not (x == y)
-- a je to :)
x /= y = not (x == y)Bez lidske inteligence si nemuze poradit ani s takovou trivialitou jako je treba odvozeni funkce (operatoru) nerovnosti:
Docela mě překvapuje, že to nevrátí třeba x /= y = True.
Příkaz Auto zvládne doplnit i složitější výrazy. Například return a bind pro stavovou monádu doplní takto:
record Pair (A B : Set) : Set where
constructor _,_
field
proj₁ : A
proj₂ : B
record State (S A : Set) : Set where
constructor state
field
runState : S → Pair S A
-- vygenerovane prikazem Auto
return : {S A : Set} → A → State S A
return x = state (λ z → z , x)
-- vygenerovane prikazem Auto (a spatne)
bind : {S A B : Set} → State S A → (A → State S B) → State S B
bind m f = state
(λ z →
z ,
Pair.proj₂
(State.runState (f (Pair.proj₂ (State.runState m z))) z))
bind je bohužel špatně – typ totiž nezakazuje použití původního stavu. Když ale umožním, aby se typ stavu měnil (pak už to není monáda), tak Auto vygeneruje již korektní definici i pro bind:
record IState (S₁ S₂ A : Set) : Set where
constructor state
field
runState : S₁ → Pair S₂ A
-- vygenerovane prikazem Auto
ibind : {S₁ S₂ S₃ A B : Set} → IState S₁ S₂ A → (A → IState S₂ S₃ B) → IState S₁ S₃ B
ibind m f = state
(λ z →
Pair.proj₁
(IState.runState (f (Pair.proj₂ (IState.runState m z)))
(Pair.proj₁ (IState.runState m z)))
,
Pair.proj₂
(IState.runState (f (Pair.proj₂ (IState.runState m z)))
(Pair.proj₁ (IState.runState m z))))
Nicméně perfektní to není – některé výrazy se tam zbytečně opakují, člověk by napsal:
-- napsane clovekem
ibind' : {S₁ S₂ S₃ A B : Set} → IState S₁ S₂ A → (A → IState S₂ S₃ B) → IState S₁ S₃ B
ibind' m f = state
(λ st₁ →
let (st₂ , a) = IState.runState m st₁
in IState.runState (f a) st₂)
IMHO to ale moc prakticky neni.Hodí se to v důkazech. Tam potřebuji najít term s daným typem a už příliš nezáleží na tom, jak ten term vypadá.
18.2.2013 13:38
coder | skóre: 4
| blog: lINUKS
18.2.2013 21:00
Josef Kufner | skóre: 70
19.2.2013 15:28
coder | skóre: 4
| blog: lINUKS
Bez Vimu si jiz nedokazi predstavit svuj zivot 
Ale ten Emacs ma spousty zajimavych funkci a doplnku, ktere bych rad pouzival a ve svete vimu jsou nedokonale imitovane. Napr. org mod a velmi kvalitni integrace REPLu funkcionalnich jazyku. No uvidim, treba se nekdy hacknu.
Hm, moc tomu nerozumim
Máte nějaký konkrétní dotaz, třeba bych mohl pomoci?
Mně se na Agdě a podobných jazycích líbí minimalističnost kombinovaná se silou typového systému. Naopak mi vadí absence aktuální definice jazyka – bylo by super, kdyby někdo zpracoval definici na úrovni Standard ML (viz stará verze: The Definition of Standard ML - Version 2).
Hlavní využití příkazu Auto je při hledání důkazů – tam totiž jde pouze o nalezení termu s odpovídajícím typem a je jedno, jak ten term vypadá. Je tohle odpověď na vaši otázku?
int f(int a, int b)a editor me k tomu doplnil:
{
return a + b;
}
i kdyz jsem mohl chtit odcitani, nasobeni, nebo neco slozitejsiho?
i kdyz jsem mohl chtit odcitani, nasobeni, nebo neco slozitejsiho?
Přesně tak. Například, když chci odčítání a použiji typ
binop₁ : ℕ → ℕ → ℕ
tak dostanu
binop₁ a b = b
což není odčítání. Musím tedy upřesnit typ:
binop₂ : (x : ℕ) → (y : ℕ) → Pair ℕ (minus_pred x y)
Místo pouhého čísla vracím dvojici. První prvek dvojice je číslo a druhý prvek je důkaz, že první prvek je rozdíl x a y. Odečítání definuji následovně:
_∸_ : ℕ → ℕ → ℕ m ∸ zero = m zero ∸ _ = zero suc m ∸ suc n = m ∸ n
Rovnost vyjadřuji pomocí následujícího typu. Typ je navržen tak, že term refl typu a ≡ b jde zkonstruovat pouze tehdy, jsou-li a a b stejné:
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
Následuje definice závislého páru, kde typ druhé složky závisí na hodnotě první složky:
record Pair (A : Set) (B : A → Set) : Set where
constructor _,_
field
proj₁ : A
proj₂ : B proj₁
Nastavení parseru:
infixl 6 _∸_ infix 4 _≡_ _,_
Funkce vracející typ (tj. výrok), že rozdíl prvních dvou čísel je roven třetímu číslu:
minus_pred : ℕ → ℕ → ℕ → Set minus_pred x y res = x ∸ y ≡ res
Pro tento typ už příkaz Auto vygeneruje požadovanou funkci:
binop₂ : (x : ℕ) → (y : ℕ) → Pair ℕ (minus_pred x y) binop₂ a b = a ∸ b , refl
24.2.2013 22:50
Josef Kufner | skóre: 70
Myslím, že neuniká. V ničem to není lepší. Je to jen příklad, že vlastnost výsledku funkce jde specifikovat typem. V tomto případě to však nemá žádné výhody – spíše naopak.
Příklad praktického použití je třeba funkce, která transformuje program a kde chceme, aby výsledný program dával stejné výsledky jako původní program.
25.2.2013 11:02
Josef Kufner | skóre: 70
Příklad praktického použití je třeba funkce, která transformuje program a kde chceme, aby výsledný program dával stejné výsledky jako původní program.Tohle větou jsi měl celý článek uvést
Vygenerovalo by to neco i kdybych nenadefinoval operator _-_ a minus_pred definoval jinym zpusobem - treba pomoci scitani?
Nejspíš ne.
Konkrétně, pokud máte na mysli podobnou definici
minus_pred : ℕ → ℕ → ℕ → Set minus_pred x y res = y + res ≡ x
tak ne. Problém je v tom, že pro x < y neexistuje přirozené číslo res a Auto hledá totální funkci (všude definovanou).
Kdybych zadefinoval relaci ≥ a funkci binop₂ definoval pouze pro x ≥ y, tak by to stejně nenašel – je to už příliš složité. Nezkoušel jsem to, ale myslím, že by se muselo nadefinovat ∸, pak dokázat lemma, že z x ≥ y a x ∸ y ≡ res plyne y + res ≡ x, a pak by to našel (ale to už není příliš zajímavé, protože je to vlastně celé hotové).
Tiskni
Sdílej:
